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

Metamath Proof Explorer

Theorem reusv2lem1

Description: Lemma for reusv2 . (Contributed by NM, 22-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reusv2lem1 
|- ( A =/= (/) -> ( E! x A. y e. A x = B <-> E. x A. y e. A x = B ) )

Proof

Step Hyp Ref Expression
1 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
2 nfra1 
 |-  F/ y A. y e. A x = B
3 2 nfmov 
 |-  F/ y E* x A. y e. A x = B
4 rsp 
 |-  ( A. y e. A x = B -> ( y e. A -> x = B ) )
5 4 com12 
 |-  ( y e. A -> ( A. y e. A x = B -> x = B ) )
6 5 alrimiv 
 |-  ( y e. A -> A. x ( A. y e. A x = B -> x = B ) )
7 mo2icl 
 |-  ( A. x ( A. y e. A x = B -> x = B ) -> E* x A. y e. A x = B )
8 6 7 syl 
 |-  ( y e. A -> E* x A. y e. A x = B )
9 3 8 exlimi 
 |-  ( E. y y e. A -> E* x A. y e. A x = B )
10 1 9 sylbi 
 |-  ( A =/= (/) -> E* x A. y e. A x = B )
11 df-eu 
 |-  ( E! x A. y e. A x = B <-> ( E. x A. y e. A x = B /\ E* x A. y e. A x = B ) )
12 11 rbaib 
 |-  ( E* x A. y e. A x = B -> ( E! x A. y e. A x = B <-> E. x A. y e. A x = B ) )
13 10 12 syl 
 |-  ( A =/= (/) -> ( E! x A. y e. A x = B <-> E. x A. y e. A x = B ) )