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 ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃! x ∃! y ∃ x φ ∧ ∃ y φ

Proof

Step Hyp Ref Expression
1 nfe1 ⊢ Ⅎ x ∃ x φ
2 1 nfeu ⊢ Ⅎ x ∃! y ∃ x φ
3 2 euan ⊢ ∃! x ∃! y ∃ x φ ∧ ∃ y φ ↔ ∃! y ∃ x φ ∧ ∃! x ∃ y φ
4 ancom ⊢ ∃ x φ ∧ ∃ y φ ↔ ∃ y φ ∧ ∃ x φ
5 4 eubii ⊢ ∃! y ∃ x φ ∧ ∃ y φ ↔ ∃! y ∃ y φ ∧ ∃ x φ
6 nfe1 ⊢ Ⅎ y ∃ y φ
7 6 euan ⊢ ∃! y ∃ y φ ∧ ∃ x φ ↔ ∃ y φ ∧ ∃! y ∃ x φ
8 ancom ⊢ ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃! y ∃ x φ ∧ ∃ y φ
9 5 7 8 3bitri ⊢ ∃! y ∃ x φ ∧ ∃ y φ ↔ ∃! y ∃ x φ ∧ ∃ y φ
10 9 eubii ⊢ ∃! x ∃! y ∃ x φ ∧ ∃ y φ ↔ ∃! x ∃! y ∃ x φ ∧ ∃ y φ
11 ancom ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃! y ∃ x φ ∧ ∃! x ∃ y φ
12 3 10 11 3bitr4ri ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃! x ∃! y ∃ x φ ∧ ∃ y φ