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

Theorem abbi 2545
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 2429 . 2  |-  ( { x  |  ph }  =  { x  |  ps } 
<-> 
A. y ( y  e.  { x  | 
ph }  <->  y  e.  { x  |  ps }
) )
2 nfsab1 2425 . . . 4  |-  F/ x  y  e.  { x  |  ph }
3 nfsab1 2425 . . . 4  |-  F/ x  y  e.  { x  |  ps }
42, 3nfbi 1856 . . 3  |-  F/ x
( y  e.  {
x  |  ph }  <->  y  e.  { x  |  ps } )
5 nfv 1629 . . 3  |-  F/ y ( ph  <->  ps )
6 df-clab 2422 . . . . 5  |-  ( y  e.  { x  | 
ph }  <->  [ y  /  x ] ph )
7 sbequ12r 1945 . . . . 5  |-  ( y  =  x  ->  ( [ y  /  x ] ph  <->  ph ) )
86, 7syl5bb 249 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
9 df-clab 2422 . . . . 5  |-  ( y  e.  { x  |  ps }  <->  [ y  /  x ] ps )
10 sbequ12r 1945 . . . . 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 1982 . 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 1549    = wceq 1652   [wsb 1658    e. wcel 1725   {cab 2421
This theorem is referenced by:  abbii  2547  abbid  2548  rabbi  2878  dfiota2  5411  iotabi  5419  uniabio  5420  iotanul  5425  karden  7811  iuneq12daf  23999  iuneq12df  24000  elnev  27606  csbingVD  28933  csbsngVD  28942  csbxpgVD  28943  csbrngVD  28945  csbunigVD  28947  csbfv12gALTVD  28948
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428
  Copyright terms: Public domain W3C validator