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

Metamath Proof Explorer

Theorem reusv2lem3

Description: Lemma for reusv2 . (Contributed by NM, 14-Dec-2012) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> E! x E. y e. A x = B )
2 nfv 
 |-  F/ x A. y e. A B e. _V
3 nfeu1 
 |-  F/ x E! x E. y e. A x = B
4 2 3 nfan 
 |-  F/ x ( A. y e. A B e. _V /\ E! x E. y e. A x = B )
5 euex 
 |-  ( E! x E. y e. A x = B -> E. x E. y e. A x = B )
6 rexn0 
 |-  ( E. y e. A x = B -> A =/= (/) )
7 6 exlimiv 
 |-  ( E. x E. y e. A x = B -> A =/= (/) )
8 r19.2z 
 |-  ( ( A =/= (/) /\ A. y e. A x = B ) -> E. y e. A x = B )
9 8 ex 
 |-  ( A =/= (/) -> ( A. y e. A x = B -> E. y e. A x = B ) )
10 5 7 9 3syl 
 |-  ( E! x E. y e. A x = B -> ( A. y e. A x = B -> E. y e. A x = B ) )
11 10 adantl 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( A. y e. A x = B -> E. y e. A x = B ) )
12 nfra1 
 |-  F/ y A. y e. A B e. _V
13 nfre1 
 |-  F/ y E. y e. A x = B
14 13 nfeuw 
 |-  F/ y E! x E. y e. A x = B
15 12 14 nfan 
 |-  F/ y ( A. y e. A B e. _V /\ E! x E. y e. A x = B )
16 rsp 
 |-  ( A. y e. A B e. _V -> ( y e. A -> B e. _V ) )
17 16 impcom 
 |-  ( ( y e. A /\ A. y e. A B e. _V ) -> B e. _V )
18 isset 
 |-  ( B e. _V <-> E. x x = B )
19 17 18 sylib 
 |-  ( ( y e. A /\ A. y e. A B e. _V ) -> E. x x = B )
20 19 adantrr 
 |-  ( ( y e. A /\ ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) ) -> E. x x = B )
21 rspe 
 |-  ( ( y e. A /\ x = B ) -> E. y e. A x = B )
22 21 ex 
 |-  ( y e. A -> ( x = B -> E. y e. A x = B ) )
23 22 ancrd 
 |-  ( y e. A -> ( x = B -> ( E. y e. A x = B /\ x = B ) ) )
24 23 eximdv 
 |-  ( y e. A -> ( E. x x = B -> E. x ( E. y e. A x = B /\ x = B ) ) )
25 24 imp 
 |-  ( ( y e. A /\ E. x x = B ) -> E. x ( E. y e. A x = B /\ x = B ) )
26 20 25 syldan 
 |-  ( ( y e. A /\ ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) ) -> E. x ( E. y e. A x = B /\ x = B ) )
27 eupick 
 |-  ( ( E! x E. y e. A x = B /\ E. x ( E. y e. A x = B /\ x = B ) ) -> ( E. y e. A x = B -> x = B ) )
28 1 26 27 syl2an2 
 |-  ( ( y e. A /\ ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) ) -> ( E. y e. A x = B -> x = B ) )
29 28 ex 
 |-  ( y e. A -> ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( E. y e. A x = B -> x = B ) ) )
30 29 com3l 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( E. y e. A x = B -> ( y e. A -> x = B ) ) )
31 15 13 30 ralrimd 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( E. y e. A x = B -> A. y e. A x = B ) )
32 11 31 impbid 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( A. y e. A x = B <-> E. y e. A x = B ) )
33 4 32 eubid 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> ( E! x A. y e. A x = B <-> E! x E. y e. A x = B ) )
34 1 33 mpbird 
 |-  ( ( A. y e. A B e. _V /\ E! x E. y e. A x = B ) -> E! x A. y e. A x = B )
35 34 ex 
 |-  ( A. y e. A B e. _V -> ( E! x E. y e. A x = B -> E! x A. y e. A x = B ) )
36 reusv2lem2 
 |-  ( E! x A. y e. A x = B -> E! x E. y e. A x = B )
37 35 36 impbid1 
 |-  ( A. y e. A B e. _V -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )