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

Theorem abbi 2527
Description: Equivalent wff's correspond to equal class abstractions. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)
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 hbab1 2384 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
2 hbab1 2384 . . 3  |-  ( y  e.  { x  |  ps }  ->  A. x  y  e.  { x  |  ps } )
31, 2cleqh 2511 . 2  |-  ( { x  |  ph }  =  { x  |  ps } 
<-> 
A. x ( x  e.  { x  | 
ph }  <->  x  e.  { x  |  ps }
) )
4 abid 2383 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
5 abid 2383 . . . 4  |-  ( x  e.  { x  |  ps }  <->  ps )
64, 5bibi12i 313 . . 3  |-  ( ( x  e.  { x  |  ph }  <->  x  e.  { x  |  ps }
)  <->  ( ph  <->  ps )
)
76albii 1655 . 2  |-  ( A. x ( x  e. 
{ x  |  ph } 
<->  x  e.  { x  |  ps } )  <->  A. x
( ph  <->  ps ) )
83, 7bitr2i 250 1  |-  ( A. x ( ph  <->  ps )  <->  { x  |  ph }  =  { x  |  ps } )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1397    = wceq 1399    e. wcel 1836   {cab 2381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2382  df-cleq 2388  df-clel 2391
This theorem is referenced by:  abbii  2530  abbid  2531  nabbi  2729  nabbiOLD  2730  rabbi  2978  sbcbi2  3318  iuneq12df  4284  dfiota2  5478  iotabi  5486  uniabio  5487  iotanul  5492  karden  8248  iuneq12daf  27583  abeq12  30770  elnev  31553  rabeqsn  33158  csbingVD  34070  csbsngVD  34079  csbxpgVD  34080  csbrngVD  34082  csbunigVD  34084  csbfv12gALTVD  34085  bj-cleq  34906
  Copyright terms: Public domain W3C validator