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

Metamath Proof Explorer

Theorem 2eu7

Description: Two equivalent expressions for double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 19-Feb-2005) (New usage is discouraged.)

Ref Expression
Assertion 2eu7 ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑
2 1 nfeu ⊢ Ⅎ 𝑥 ∃! 𝑦 ∃ 𝑥 𝜑
3 2 euan ⊢ ( ∃! 𝑥 ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) )
4 ancom ⊢ ( ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃ 𝑥 𝜑 ) )
5 4 eubii ⊢ ( ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑦 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑥 𝜑 ) )
6 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑
7 6 euan ⊢ ( ∃! 𝑦 ( ∃ 𝑦 𝜑 ∧ ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) )
8 ancom ⊢ ( ( ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
9 5 7 8 3bitri ⊢ ( ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
10 9 eubii ⊢ ( ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) ↔ ∃! 𝑥 ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )
11 ancom ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃! 𝑦 ∃ 𝑥 𝜑 ∧ ∃! 𝑥 ∃ 𝑦 𝜑 ) )
12 3 10 11 3bitr4ri ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃! 𝑥 ∃! 𝑦 ( ∃ 𝑥 𝜑 ∧ ∃ 𝑦 𝜑 ) )