Theorem euxfr 1436

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A.

Hypotheses

Ref	Expression
euxfr.1	⊢ A ∈ V
euxfr.2	⊢ ∃!y x = A
euxfr.3	⊢ (x = A → (φ ↔ ψ))

Assertion

Ref	Expression
euxfr	⊢ (∃!xφ ↔ ∃!yψ)

Distinct variable group(s):   ψ,x   φ,y   x,A   x,y

Proof of Theorem euxfr

Step	Hyp	Ref	Expression
1		euxfr.2	. . . . . . 7 ⊢ ∃!y x = A
2		euex 1021	. . . . . . 7 ⊢ (∃!y x = A → ∃y x = A)
3	1, 2	ax-mp 6	. . . . . 6 ⊢ ∃y x = A
4	3	biantrur 544	. . . . 5 ⊢ (φ ↔ (∃y x = A ∧ φ))
5		19.41v 963	. . . . 5 ⊢ (∃y(x = A ∧ φ) ↔ (∃y x = A ∧ φ))
6	4, 5	bitr4 154	. . . 4 ⊢ (φ ↔ ∃y(x = A ∧ φ))
7		euxfr.3	. . . . . 6 ⊢ (x = A → (φ ↔ ψ))
8	7	pm5.32i 489	. . . . 5 ⊢ ((x = A ∧ φ) ↔ (x = A ∧ ψ))
9	8	biex 733	. . . 4 ⊢ (∃y(x = A ∧ φ) ↔ ∃y(x = A ∧ ψ))
10	6, 9	bitr 151	. . 3 ⊢ (φ ↔ ∃y(x = A ∧ ψ))
11	10	bieu 1014	. 2 ⊢ (∃!xφ ↔ ∃!x∃y(x = A ∧ ψ))
12		euxfr.1	. . 3 ⊢ A ∈ V
13	1	eumoi 1038	. . 3 ⊢ ∃*y x = A
14	12, 13	euxfr2 1435	. 2 ⊢ (∃!x∃y(x = A ∧ ψ) ↔ ∃!yψ)
15	11, 14	bitr 151	1 ⊢ (∃!xφ ↔ ∃!yψ)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678  ∃!weu 1007   = wceq 1091   ∈ wcel 1092  Vcvv 1348

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org