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

Theorem abbi 2406
Description: Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
abbi  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )

Proof of Theorem abbi
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2290 . 2  |-  ( { x  |  ph }  =  { x  |  ps } 
<-> 
A. y ( y  e.  { x  | 
ph }  <->  y  e.  { x  |  ps }
) )
2 nfsab1 2286 . . . 4  |-  F/ x  y  e.  { x  |  ph }
3 nfsab1 2286 . . . 4  |-  F/ x  y  e.  { x  |  ps }
42, 3nfbi 1784 . . 3  |-  F/ x
( y  e.  {
x  |  ph }  <->  y  e.  { x  |  ps } )
5 nfv 1609 . . 3  |-  F/ y ( ph  <->  ps )
6 df-clab 2283 . . . . 5  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
7 sbequ12r 1873 . . . . 5  |-  ( y  =  x  ->  ( [ y  /  x ] ph  <->  ph ) )
86, 7syl5bb 248 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
9 df-clab 2283 . . . . 5  |-  ( y  e.  { x  |  ps }  <->  [ y  /  x ] ps )
10 sbequ12r 1873 . . . . 5  |-  ( y  =  x  ->  ( [ y  /  x ] ps  <->  ps ) )
119, 10syl5bb 248 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ps }  <->  ps )
)
128, 11bibi12d 312 . . 3  |-  ( y  =  x  ->  (
( y  e.  {
x  |  ph }  <->  y  e.  { x  |  ps } )  <->  ( ph  <->  ps ) ) )
134, 5, 12cbval 1937 . 2  |-  ( A. y ( y  e. 
{ x  |  ph } 
<->  y  e.  { x  |  ps } )  <->  A. x
( ph  <->  ps ) )
141, 13bitr2i 241 1  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530    = wceq 1632   [wsb 1638    e. wcel 1696   {cab 2282
This theorem is referenced by:  abbii  2408  abbid  2409  rabbi  2731  dfiota2  5236  iotabi  5244  uniabio  5245  iotanul  5250  karden  7581  iuneq12daf  23170  iuneq12df  23171  rabbidva2  23180  elnev  27741  csbingVD  28976  csbsngVD  28985  csbxpgVD  28986  csbrngVD  28988  csbunigVD  28990  csbfv12gALTVD  28991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289
  Copyright terms: Public domain W3C validator