MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reusv2lem4 Unicode version

Theorem reusv2lem4 4538
Description: Lemma for reusv2 4540. (Contributed by NM, 13-Dec-2012.)
Assertion
Ref Expression
reusv2lem4  |-  ( E! x  e.  A  E. y  e.  B  ( ph  /\  x  =  C )  <->  E! x A. y  e.  B  ( ( C  e.  A  /\  ph )  ->  x  =  C ) )
Distinct variable groups:    x, y, A    x, B    x, C    ph, x
Allowed substitution hints:    ph( y)    B( y)    C( y)

Proof of Theorem reusv2lem4
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-reu 2550 . 2  |-  ( 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 630 . . . . . . 7  |-  ( ( ( y  e.  B  /\  ( C  e.  A  /\  ph ) )  /\  x  =  C )  <->  ( y  e.  B  /\  ( ( C  e.  A  /\  ph )  /\  x  =  C
) ) )
32bicomi 193 . . . . . 6  |-  ( ( y  e.  B  /\  ( ( C  e.  A  /\  ph )  /\  x  =  C
) )  <->  ( (
y  e.  B  /\  ( C  e.  A  /\  ph ) )  /\  x  =  C )
)
4 anass 630 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  ph )  /\  x  =  C )  <->  ( x  e.  A  /\  ( ph  /\  x  =  C ) ) )
5 eleq1 2343 . . . . . . . . . 10  |-  ( x  =  C  ->  (
x  e.  A  <->  C  e.  A ) )
65anbi1d 685 . . . . . . . . 9  |-  ( x  =  C  ->  (
( x  e.  A  /\  ph )  <->  ( C  e.  A  /\  ph )
) )
76pm5.32ri 619 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  ph )  /\  x  =  C )  <->  ( ( C  e.  A  /\  ph )  /\  x  =  C ) )
84, 7bitr3i 242 . . . . . . 7  |-  ( ( x  e.  A  /\  ( ph  /\  x  =  C ) )  <->  ( ( C  e.  A  /\  ph )  /\  x  =  C ) )
98anbi2i 675 . . . . . 6  |-  ( ( y  e.  B  /\  ( x  e.  A  /\  ( ph  /\  x  =  C ) ) )  <-> 
( y  e.  B  /\  ( ( C  e.  A  /\  ph )  /\  x  =  C
) ) )
10 rabid 2716 . . . . . . 7  |-  ( y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  <->  ( y  e.  B  /\  ( C  e.  A  /\  ph ) ) )
1110anbi1i 676 . . . . . 6  |-  ( ( y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  /\  x  =  C )  <->  ( (
y  e.  B  /\  ( C  e.  A  /\  ph ) )  /\  x  =  C )
)
123, 9, 113bitr4i 268 . . . . 5  |-  ( ( y  e.  B  /\  ( x  e.  A  /\  ( ph  /\  x  =  C ) ) )  <-> 
( y  e.  {
y  e.  B  | 
( C  e.  A  /\  ph ) }  /\  x  =  C )
)
1312rexbii2 2572 . . . 4  |-  ( E. y  e.  B  ( x  e.  A  /\  ( ph  /\  x  =  C ) )  <->  E. y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) } x  =  C
)
14 r19.42v 2694 . . . 4  |-  ( E. y  e.  B  ( x  e.  A  /\  ( ph  /\  x  =  C ) )  <->  ( x  e.  A  /\  E. y  e.  B  ( ph  /\  x  =  C ) ) )
15 nfrab1 2720 . . . . 5  |-  F/_ y { y  e.  B  |  ( C  e.  A  /\  ph ) }
16 nfcv 2419 . . . . 5  |-  F/_ z { y  e.  B  |  ( C  e.  A  /\  ph ) }
17 nfv 1605 . . . . 5  |-  F/ z  x  =  C
18 nfcsb1v 3113 . . . . . 6  |-  F/_ y [_ z  /  y ]_ C
1918nfeq2 2430 . . . . 5  |-  F/ y  x  =  [_ z  /  y ]_ C
20 csbeq1a 3089 . . . . . 6  |-  ( y  =  z  ->  C  =  [_ z  /  y ]_ C )
2120eqeq2d 2294 . . . . 5  |-  ( y  =  z  ->  (
x  =  C  <->  x  =  [_ z  /  y ]_ C ) )
2215, 16, 17, 19, 21cbvrexf 2759 . . . 4  |-  ( 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 )
2313, 14, 223bitr3i 266 . . 3  |-  ( ( x  e.  A  /\  E. y  e.  B  (
ph  /\  x  =  C ) )  <->  E. z  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) } x  =  [_ z  /  y ]_ C
)
2423eubii 2152 . 2  |-  ( 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
)
25 elex 2796 . . . . . . . 8  |-  ( C  e.  A  ->  C  e.  _V )
2625ad2antrl 708 . . . . . . 7  |-  ( ( y  e.  B  /\  ( C  e.  A  /\  ph ) )  ->  C  e.  _V )
2710, 26sylbi 187 . . . . . 6  |-  ( y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  ->  C  e. 
_V )
2827rgen 2608 . . . . 5  |-  A. y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) } C  e.  _V
29 nfv 1605 . . . . . 6  |-  F/ z  C  e.  _V
3018nfel1 2429 . . . . . 6  |-  F/ y
[_ z  /  y ]_ C  e.  _V
3120eleq1d 2349 . . . . . 6  |-  ( y  =  z  ->  ( C  e.  _V  <->  [_ z  / 
y ]_ C  e.  _V ) )
3215, 16, 29, 30, 31cbvralf 2758 . . . . 5  |-  ( 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 )
3328, 32mpbi 199 . . . 4  |-  A. z  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) } [_ z  /  y ]_ C  e.  _V
34 reusv2lem3 4537 . . . 4  |-  ( 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
) )
3533, 34ax-mp 8 . . 3  |-  ( 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
)
36 df-ral 2548 . . . . 5  |-  ( 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 ) )
37 nfv 1605 . . . . . 6  |-  F/ z ( y  e.  {
y  e.  B  | 
( C  e.  A  /\  ph ) }  ->  x  =  C )
3815nfel2 2431 . . . . . . 7  |-  F/ y  z  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }
3938, 19nfim 1769 . . . . . 6  |-  F/ y ( z  e.  {
y  e.  B  | 
( C  e.  A  /\  ph ) }  ->  x  =  [_ z  / 
y ]_ C )
40 eleq1 2343 . . . . . . 7  |-  ( y  =  z  ->  (
y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  <->  z  e.  { y  e.  B  | 
( C  e.  A  /\  ph ) } ) )
4140, 21imbi12d 311 . . . . . 6  |-  ( 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
) ) )
4237, 39, 41cbval 1924 . . . . 5  |-  ( 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 ) )
4310imbi1i 315 . . . . . . . 8  |-  ( ( y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  ->  x  =  C )  <->  ( (
y  e.  B  /\  ( C  e.  A  /\  ph ) )  ->  x  =  C )
)
44 impexp 433 . . . . . . . 8  |-  ( ( ( y  e.  B  /\  ( C  e.  A  /\  ph ) )  ->  x  =  C )  <->  ( y  e.  B  -> 
( ( C  e.  A  /\  ph )  ->  x  =  C ) ) )
4543, 44bitri 240 . . . . . . 7  |-  ( ( y  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) }  ->  x  =  C )  <->  ( y  e.  B  ->  ( ( C  e.  A  /\  ph )  ->  x  =  C ) ) )
4645albii 1553 . . . . . 6  |-  ( A. y ( y  e. 
{ y  e.  B  |  ( C  e.  A  /\  ph ) }  ->  x  =  C )  <->  A. y ( y  e.  B  ->  (
( C  e.  A  /\  ph )  ->  x  =  C ) ) )
47 df-ral 2548 . . . . . 6  |-  ( A. y  e.  B  (
( C  e.  A  /\  ph )  ->  x  =  C )  <->  A. y
( y  e.  B  ->  ( ( C  e.  A  /\  ph )  ->  x  =  C ) ) )
4846, 47bitr4i 243 . . . . 5  |-  ( A. y ( y  e. 
{ y  e.  B  |  ( C  e.  A  /\  ph ) }  ->  x  =  C )  <->  A. y  e.  B  ( ( C  e.  A  /\  ph )  ->  x  =  C ) )
4936, 42, 483bitr2i 264 . . . 4  |-  ( A. z  e.  { y  e.  B  |  ( C  e.  A  /\  ph ) } x  = 
[_ z  /  y ]_ C  <->  A. y  e.  B  ( ( C  e.  A  /\  ph )  ->  x  =  C ) )
5049eubii 2152 . . 3  |-  ( 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 ) )
5135, 50bitri 240 . 2  |-  ( 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 ) )
521, 24, 513bitri 262 1  |-  ( E! x  e.  A  E. y  e.  B  ( ph  /\  x  =  C )  <->  E! x A. y  e.  B  ( ( C  e.  A  /\  ph )  ->  x  =  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527    = wceq 1623    e. wcel 1684   E!weu 2143   A.wral 2543   E.wrex 2544   E!wreu 2545   {crab 2547   _Vcvv 2788   [_csb 3081
This theorem is referenced by:  reusv2lem5  4539  reusv7OLD  4546
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149  ax-pow 4188
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator