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

Metamath Proof Explorer

Theorem reusv2lem2

Description: Lemma for reusv2 . (Contributed by NM, 27-Oct-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 eunex 
 |-  ( E! x A. y e. A x = B -> E. x -. A. y e. A x = B )
2 exnal 
 |-  ( E. x -. A. y e. A x = B <-> -. A. x A. y e. A x = B )
3 1 2 sylib 
 |-  ( E! x A. y e. A x = B -> -. A. x A. y e. A x = B )
4 rzal 
 |-  ( A = (/) -> A. y e. A x = B )
5 4 alrimiv 
 |-  ( A = (/) -> A. x A. y e. A x = B )
6 3 5 nsyl3 
 |-  ( A = (/) -> -. E! x A. y e. A x = B )
7 6 pm2.21d 
 |-  ( A = (/) -> ( E! x A. y e. A x = B -> E! x E. y e. A x = B ) )
8 simpr 
 |-  ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> E! x A. y e. A x = B )
9 nfra1 
 |-  F/ y A. y e. A z = B
10 nfra1 
 |-  F/ y A. y e. A x = B
11 simpr 
 |-  ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> x = B )
12 rspa 
 |-  ( ( A. y e. A z = B /\ y e. A ) -> z = B )
13 12 adantr 
 |-  ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> z = B )
14 11 13 eqtr4d 
 |-  ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> x = z )
15 eqeq1 
 |-  ( x = z -> ( x = B <-> z = B ) )
16 15 ralbidv 
 |-  ( x = z -> ( A. y e. A x = B <-> A. y e. A z = B ) )
17 16 biimprcd 
 |-  ( A. y e. A z = B -> ( x = z -> A. y e. A x = B ) )
18 17 ad2antrr 
 |-  ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> ( x = z -> A. y e. A x = B ) )
19 14 18 mpd 
 |-  ( ( ( A. y e. A z = B /\ y e. A ) /\ x = B ) -> A. y e. A x = B )
20 19 exp31 
 |-  ( A. y e. A z = B -> ( y e. A -> ( x = B -> A. y e. A x = B ) ) )
21 9 10 20 rexlimd 
 |-  ( A. y e. A z = B -> ( E. y e. A x = B -> A. y e. A x = B ) )
22 21 adantl 
 |-  ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E. y e. A x = B -> A. y e. A x = B ) )
23 r19.2z 
 |-  ( ( A =/= (/) /\ A. y e. A x = B ) -> E. y e. A x = B )
24 23 ex 
 |-  ( A =/= (/) -> ( A. y e. A x = B -> E. y e. A x = B ) )
25 24 adantr 
 |-  ( ( A =/= (/) /\ A. y e. A z = B ) -> ( A. y e. A x = B -> E. y e. A x = B ) )
26 22 25 impbid 
 |-  ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E. y e. A x = B <-> A. y e. A x = B ) )
27 26 eubidv 
 |-  ( ( A =/= (/) /\ A. y e. A z = B ) -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
28 27 ex 
 |-  ( A =/= (/) -> ( A. y e. A z = B -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) ) )
29 28 exlimdv 
 |-  ( A =/= (/) -> ( E. z A. y e. A z = B -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) ) )
30 euex 
 |-  ( E! x A. y e. A x = B -> E. x A. y e. A x = B )
31 16 cbvexvw 
 |-  ( E. x A. y e. A x = B <-> E. z A. y e. A z = B )
32 30 31 sylib 
 |-  ( E! x A. y e. A x = B -> E. z A. y e. A z = B )
33 29 32 impel 
 |-  ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
34 8 33 mpbird 
 |-  ( ( A =/= (/) /\ E! x A. y e. A x = B ) -> E! x E. y e. A x = B )
35 34 ex 
 |-  ( A =/= (/) -> ( E! x A. y e. A x = B -> E! x E. y e. A x = B ) )
36 7 35 pm2.61ine 
 |-  ( E! x A. y e. A x = B -> E! x E. y e. A x = B )