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

Theorem rabbi 3040
Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3104. (Contributed by NM, 25-Nov-2013.)
Assertion
Ref Expression
rabbi  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  { x  e.  A  |  ps }  =  { x  e.  A  |  ch } )

Proof of Theorem rabbi
StepHypRef Expression
1 abbi 2598 . 2  |-  ( A. x ( ( x  e.  A  /\  ps ) 
<->  ( x  e.  A  /\  ch ) )  <->  { x  |  ( x  e.  A  /\  ps ) }  =  { x  |  ( x  e.  A  /\  ch ) } )
2 df-ral 2819 . . 3  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  A. x
( x  e.  A  ->  ( ps  <->  ch )
) )
3 pm5.32 636 . . . 4  |-  ( ( x  e.  A  -> 
( ps  <->  ch )
)  <->  ( ( x  e.  A  /\  ps ) 
<->  ( x  e.  A  /\  ch ) ) )
43albii 1620 . . 3  |-  ( A. x ( x  e.  A  ->  ( ps  <->  ch ) )  <->  A. x
( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
52, 4bitri 249 . 2  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  A. x
( ( x  e.  A  /\  ps )  <->  ( x  e.  A  /\  ch ) ) )
6 df-rab 2823 . . 3  |-  { x  e.  A  |  ps }  =  { x  |  ( x  e.  A  /\  ps ) }
7 df-rab 2823 . . 3  |-  { x  e.  A  |  ch }  =  { x  |  ( x  e.  A  /\  ch ) }
86, 7eqeq12i 2487 . 2  |-  ( { x  e.  A  |  ps }  =  { x  e.  A  |  ch } 
<->  { x  |  ( x  e.  A  /\  ps ) }  =  {
x  |  ( x  e.  A  /\  ch ) } )
91, 5, 83bitr4i 277 1  |-  ( A. x  e.  A  ( ps 
<->  ch )  <->  { x  e.  A  |  ps }  =  { x  e.  A  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1377    = wceq 1379    e. wcel 1767   {cab 2452   A.wral 2814   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823
This theorem is referenced by:  rabbidva  3104  kqfeq  20052  isr0  20065  rabeq12f  30396  eq0rabdioph  30541  eqrabdioph  30542  lerabdioph  30569  eluzrabdioph  30570  ltrabdioph  30572  nerabdioph  30573  dvdsrabdioph  30574  ioodvbdlimc1lem2  31489  ioodvbdlimc2lem  31491  fourierdlem89  31723  fourierdlem91  31725  fourierdlem100  31734  fourierdlem108  31742  fourierdlem112  31746  bj-rabbida  33784
  Copyright terms: Public domain W3C validator