Theorem euxfr2

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker euxfr2w when possible. (Contributed by NM, 14-Nov-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	euxfr2.1	⊢ 𝐴 ∈ V
	euxfr2.2	⊢ ∃* 𝑦 𝑥 = 𝐴
Assertion	euxfr2	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		euxfr2.1	⊢ 𝐴 ∈ V
2		euxfr2.2	⊢ ∃* 𝑦 𝑥 = 𝐴
3		2euswap	⊢ ( ∀ 𝑥 ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
4	2	moani	⊢ ∃* 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 )
5		ancom	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ( 𝑥 = 𝐴 ∧ 𝜑 ) )
6	5	mobii	⊢ ( ∃* 𝑦 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
7	4 6	mpbi	⊢ ∃* 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 )
8	3 7	mpg	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
9		2euswap	⊢ ( ∀ 𝑦 ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ) )
10		moeq	⊢ ∃* 𝑥 𝑥 = 𝐴
11	10	moani	⊢ ∃* 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 )
12	5	mobii	⊢ ( ∃* 𝑥 ( 𝜑 ∧ 𝑥 = 𝐴 ) ↔ ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
13	11 12	mpbi	⊢ ∃* 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 )
14	9 13	mpg	⊢ ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) → ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
15	8 14	impbii	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) )
16		biidd	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜑 ) )
17	1 16	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 )
18	17	eubii	⊢ ( ∃! 𝑦 ∃ 𝑥 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )
19	15 18	bitri	⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )