Metamath Proof Explorer

Theorem 2eu5OLD

Description: Obsolete version of 2eu5 as of 2-Oct-2023. (Contributed by NM, 26-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2eu5OLD 
|- ( ( E! x E! y ph /\ A. x E* y 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 2eu1 
 |-  ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
2 1 pm5.32ri 
 |-  ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) )
3 eumo 
 |-  ( E! y E. x ph -> E* y E. x ph )
4 3 adantl 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> E* y E. x ph )
5 2moex 
 |-  ( E* y E. x ph -> A. x E* y ph )
6 4 5 syl 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) -> A. x E* y ph )
7 6 pm4.71i 
 |-  ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) )
8 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 ) ) ) )
9 2 7 8 3bitr2i 
 |-  ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )