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

Theorem abbi 2579
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 2438 . . 3  |-  ( y  e.  { x  | 
ph }  ->  A. x  y  e.  { x  |  ph } )
2 hbab1 2438 . . 3  |-  ( y  e.  { x  |  ps }  ->  A. x  y  e.  { x  |  ps } )
31, 2cleqh 2563 . 2  |-  ( { x  |  ph }  =  { x  |  ps } 
<-> 
A. x ( x  e.  { x  | 
ph }  <->  x  e.  { x  |  ps }
) )
4 abid 2437 . . . 4  |-  ( x  e.  { x  | 
ph }  <->  ph )
5 abid 2437 . . . 4  |-  ( x  e.  { x  |  ps }  <->  ps )
64, 5bibi12i 315 . . 3  |-  ( ( x  e.  { x  |  ph }  <->  x  e.  { x  |  ps }
)  <->  ( ph  <->  ps )
)
76albii 1611 . 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 1368    = wceq 1370    e. wcel 1757   {cab 2435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445
This theorem is referenced by:  abbii  2582  abbid  2583  nabbi  2778  nabbiOLD  2779  rabbi  2981  sbcbi2  3321  iuneq12df  4278  dfiota2  5466  iotabi  5474  uniabio  5475  iotanul  5480  karden  8189  iuneq12daf  26028  abeq12  29092  elnev  29816  rabeqsn  30841  csbingVD  31902  csbsngVD  31911  csbxpgVD  31912  csbrngVD  31914  csbunigVD  31916  csbfv12gALTVD  31917  bj-cleq  32736
  Copyright terms: Public domain W3C validator