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

Metamath Proof Explorer

Theorem reusv2lem4

Description: Lemma for reusv2 . (Contributed by NM, 13-Dec-2012)

Ref Expression
Assertion reusv2lem4 
|- ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x A. y e. B ( ( C e. A /\ ph ) -> x = C ) )

Proof

Step Hyp Ref Expression
1 df-reu 
 |-  ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x ( x e. A /\ E. y e. B ( ph /\ x = C ) ) )
2 anass 
 |-  ( ( ( y e. B /\ ( C e. A /\ ph ) ) /\ x = C ) <-> ( y e. B /\ ( ( C e. A /\ ph ) /\ x = C ) ) )
3 rabid 
 |-  ( y e. { y e. B | ( C e. A /\ ph ) } <-> ( y e. B /\ ( C e. A /\ ph ) ) )
4 3 anbi1i 
 |-  ( ( y e. { y e. B | ( C e. A /\ ph ) } /\ x = C ) <-> ( ( y e. B /\ ( C e. A /\ ph ) ) /\ x = C ) )
5 anass 
 |-  ( ( ( x e. A /\ ph ) /\ x = C ) <-> ( x e. A /\ ( ph /\ x = C ) ) )
6 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
7 6 anbi1d 
 |-  ( x = C -> ( ( x e. A /\ ph ) <-> ( C e. A /\ ph ) ) )
8 7 pm5.32ri 
 |-  ( ( ( x e. A /\ ph ) /\ x = C ) <-> ( ( C e. A /\ ph ) /\ x = C ) )
9 5 8 bitr3i 
 |-  ( ( x e. A /\ ( ph /\ x = C ) ) <-> ( ( C e. A /\ ph ) /\ x = C ) )
10 9 anbi2i 
 |-  ( ( y e. B /\ ( x e. A /\ ( ph /\ x = C ) ) ) <-> ( y e. B /\ ( ( C e. A /\ ph ) /\ x = C ) ) )
11 2 4 10 3bitr4ri 
 |-  ( ( y e. B /\ ( x e. A /\ ( ph /\ x = C ) ) ) <-> ( y e. { y e. B | ( C e. A /\ ph ) } /\ x = C ) )
12 11 rexbii2 
 |-  ( E. y e. B ( x e. A /\ ( ph /\ x = C ) ) <-> E. y e. { y e. B | ( C e. A /\ ph ) } x = C )
13 r19.42v 
 |-  ( E. y e. B ( x e. A /\ ( ph /\ x = C ) ) <-> ( x e. A /\ E. y e. B ( ph /\ x = C ) ) )
14 nfrab1 
 |-  F/_ y { y e. B | ( C e. A /\ ph ) }
15 nfcv 
 |-  F/_ z { y e. B | ( C e. A /\ ph ) }
16 nfv 
 |-  F/ z x = C
17 nfcsb1v 
 |-  F/_ y [_ z / y ]_ C
18 17 nfeq2 
 |-  F/ y x = [_ z / y ]_ C
19 csbeq1a 
 |-  ( y = z -> C = [_ z / y ]_ C )
20 19 eqeq2d 
 |-  ( y = z -> ( x = C <-> x = [_ z / y ]_ C ) )
21 14 15 16 18 20 cbvrexfw 
 |-  ( E. y e. { y e. B | ( C e. A /\ ph ) } x = C <-> E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C )
22 12 13 21 3bitr3i 
 |-  ( ( x e. A /\ E. y e. B ( ph /\ x = C ) ) <-> E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C )
23 22 eubii 
 |-  ( E! x ( x e. A /\ E. y e. B ( ph /\ x = C ) ) <-> E! x E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C )
24 elex 
 |-  ( C e. A -> C e. _V )
25 24 ad2antrl 
 |-  ( ( y e. B /\ ( C e. A /\ ph ) ) -> C e. _V )
26 3 25 sylbi 
 |-  ( y e. { y e. B | ( C e. A /\ ph ) } -> C e. _V )
27 26 rgen 
 |-  A. y e. { y e. B | ( C e. A /\ ph ) } C e. _V
28 nfv 
 |-  F/ z C e. _V
29 17 nfel1 
 |-  F/ y [_ z / y ]_ C e. _V
30 19 eleq1d 
 |-  ( y = z -> ( C e. _V <-> [_ z / y ]_ C e. _V ) )
31 14 15 28 29 30 cbvralfw 
 |-  ( A. y e. { y e. B | ( C e. A /\ ph ) } C e. _V <-> A. z e. { y e. B | ( C e. A /\ ph ) } [_ z / y ]_ C e. _V )
32 27 31 mpbi 
 |-  A. z e. { y e. B | ( C e. A /\ ph ) } [_ z / y ]_ C e. _V
33 reusv2lem3 
 |-  ( A. z e. { y e. B | ( C e. A /\ ph ) } [_ z / y ]_ C e. _V -> ( E! x E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> E! x A. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C ) )
34 32 33 ax-mp 
 |-  ( E! x E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> E! x A. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C )
35 df-ral 
 |-  ( A. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> A. z ( z e. { y e. B | ( C e. A /\ ph ) } -> x = [_ z / y ]_ C ) )
36 nfv 
 |-  F/ z ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C )
37 14 nfcri 
 |-  F/ y z e. { y e. B | ( C e. A /\ ph ) }
38 37 18 nfim 
 |-  F/ y ( z e. { y e. B | ( C e. A /\ ph ) } -> x = [_ z / y ]_ C )
39 eleq1 
 |-  ( y = z -> ( y e. { y e. B | ( C e. A /\ ph ) } <-> z e. { y e. B | ( C e. A /\ ph ) } ) )
40 39 20 imbi12d 
 |-  ( y = z -> ( ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> ( z e. { y e. B | ( C e. A /\ ph ) } -> x = [_ z / y ]_ C ) ) )
41 36 38 40 cbvalv1 
 |-  ( A. y ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> A. z ( z e. { y e. B | ( C e. A /\ ph ) } -> x = [_ z / y ]_ C ) )
42 3 imbi1i 
 |-  ( ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> ( ( y e. B /\ ( C e. A /\ ph ) ) -> x = C ) )
43 impexp 
 |-  ( ( ( y e. B /\ ( C e. A /\ ph ) ) -> x = C ) <-> ( y e. B -> ( ( C e. A /\ ph ) -> x = C ) ) )
44 42 43 bitri 
 |-  ( ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> ( y e. B -> ( ( C e. A /\ ph ) -> x = C ) ) )
45 44 albii 
 |-  ( A. y ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> A. y ( y e. B -> ( ( C e. A /\ ph ) -> x = C ) ) )
46 df-ral 
 |-  ( A. y e. B ( ( C e. A /\ ph ) -> x = C ) <-> A. y ( y e. B -> ( ( C e. A /\ ph ) -> x = C ) ) )
47 45 46 bitr4i 
 |-  ( A. y ( y e. { y e. B | ( C e. A /\ ph ) } -> x = C ) <-> A. y e. B ( ( C e. A /\ ph ) -> x = C ) )
48 35 41 47 3bitr2i 
 |-  ( A. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> A. y e. B ( ( C e. A /\ ph ) -> x = C ) )
49 48 eubii 
 |-  ( E! x A. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> E! x A. y e. B ( ( C e. A /\ ph ) -> x = C ) )
50 34 49 bitri 
 |-  ( E! x E. z e. { y e. B | ( C e. A /\ ph ) } x = [_ z / y ]_ C <-> E! x A. y e. B ( ( C e. A /\ ph ) -> x = C ) )
51 1 23 50 3bitri 
 |-  ( E! x e. A E. y e. B ( ph /\ x = C ) <-> E! x A. y e. B ( ( C e. A /\ ph ) -> x = C ) )