Metamath Proof Explorer

Theorem 2eu4

Description: This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y "). Naively one might think (incorrectly) that it could be defined by E! x E! y ph . See 2eu1 for a condition under which the naive definition holds and 2exeu for a one-way implication. See 2eu5 and 2eu8 for alternate definitions. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 14-Sep-2019)

Ref Expression
Assertion 2eu4 
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )

Proof

Step Hyp Ref Expression
1 df-eu 
 |-  ( E! x E. y ph <-> ( E. x E. y ph /\ E* x E. y ph ) )
2 df-eu 
 |-  ( E! y E. x ph <-> ( E. y E. x ph /\ E* y E. x ph ) )
3 excom 
 |-  ( E. y E. x ph <-> E. x E. y ph )
4 2 3 bianbi 
 |-  ( E! y E. x ph <-> ( E. x E. y ph /\ E* y E. x ph ) )
5 1 4 anbi12i 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( ( E. x E. y ph /\ E* x E. y ph ) /\ ( E. x E. y ph /\ E* y E. x ph ) ) )
6 anandi 
 |-  ( ( E. x E. y ph /\ ( E* x E. y ph /\ E* y E. x ph ) ) <-> ( ( E. x E. y ph /\ E* x E. y ph ) /\ ( E. x E. y ph /\ E* y E. x ph ) ) )
7 2mo2 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
8 7 anbi2i 
 |-  ( ( E. x E. y ph /\ ( E* x E. y ph /\ E* y E. x ph ) ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
9 5 6 8 3bitr2i 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )