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

Theorem abbi 2499
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 2383 . 2  |-  ( { x  |  ph }  =  { x  |  ps } 
<-> 
A. y ( y  e.  { x  | 
ph }  <->  y  e.  { x  |  ps }
) )
2 nfsab1 2379 . . . 4  |-  F/ x  y  e.  { x  |  ph }
3 nfsab1 2379 . . . 4  |-  F/ x  y  e.  { x  |  ps }
42, 3nfbi 1846 . . 3  |-  F/ x
( y  e.  {
x  |  ph }  <->  y  e.  { x  |  ps } )
5 nfv 1626 . . 3  |-  F/ y ( ph  <->  ps )
6 df-clab 2376 . . . . 5  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
7 sbequ12r 1934 . . . . 5  |-  ( y  =  x  ->  ( [ y  /  x ] ph  <->  ph ) )
86, 7syl5bb 249 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
9 df-clab 2376 . . . . 5  |-  ( y  e.  { x  |  ps }  <->  [ y  /  x ] ps )
10 sbequ12r 1934 . . . . 5  |-  ( y  =  x  ->  ( [ y  /  x ] ps  <->  ps ) )
119, 10syl5bb 249 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ps }  <->  ps )
)
128, 11bibi12d 313 . . 3  |-  ( y  =  x  ->  (
( y  e.  {
x  |  ph }  <->  y  e.  { x  |  ps } )  <->  ( ph  <->  ps ) ) )
134, 5, 12cbval 2024 . 2  |-  ( A. y ( y  e. 
{ x  |  ph } 
<->  y  e.  { x  |  ps } )  <->  A. x
( ph  <->  ps ) )
141, 13bitr2i 242 1  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546    = wceq 1649   [wsb 1655    e. wcel 1717   {cab 2375
This theorem is referenced by:  abbii  2501  abbid  2502  rabbi  2831  dfiota2  5361  iotabi  5369  uniabio  5370  iotanul  5375  karden  7754  iuneq12daf  23853  iuneq12df  23854  elnev  27309  csbingVD  28339  csbsngVD  28348  csbxpgVD  28349  csbrngVD  28351  csbunigVD  28353  csbfv12gALTVD  28354
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382
  Copyright terms: Public domain W3C validator