This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ∃! 𝑥 ∃ 𝑦 ( 𝑥 = 𝐴 ∧ 𝜑 ) ↔ ∃! 𝑦 𝜑 )