Metamath Proof Explorer


Theorem 2exeuv

Description: Version of 2exeu with x and y distinct, but not requiring ax-13 . (Contributed by Wolf Lammen, 2-Oct-2023)

Ref Expression
Assertion 2exeuv ∃! x y φ ∃! y x φ ∃! x ∃! y φ

Proof

Step Hyp Ref Expression
1 eumo ∃! x y φ * x y φ
2 euex ∃! y φ y φ
3 2 moimi * x y φ * x ∃! y φ
4 1 3 syl ∃! x y φ * x ∃! y φ
5 2euexv ∃! y x φ x ∃! y φ
6 4 5 anim12ci ∃! x y φ ∃! y x φ x ∃! y φ * x ∃! y φ
7 df-eu ∃! x ∃! y φ x ∃! y φ * x ∃! y φ
8 6 7 sylibr ∃! x y φ ∃! y x φ ∃! x ∃! y φ