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

Theorem abbi 2588
 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

Proof of Theorem abbi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 hbab1 2445 . . 3
2 hbab1 2445 . . 3
31, 2cleqh 2572 . 2
4 abid 2444 . . . 4
5 abid 2444 . . . 4
64, 5bibi12i 315 . . 3
76albii 1640 . 2
83, 7bitr2i 250 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442 This theorem is referenced by:  abbii  2591  abbid  2592  nabbi  2790  nabbiOLD  2791  rabbi  3036  sbcbi2  3378  iuneq12df  4354  dfiota2  5557  iotabi  5565  uniabio  5566  iotanul  5571  karden  8334  iuneq12daf  27425  abeq12  30564  elnev  31345  rabeqsn  32919  csbingVD  33684  csbsngVD  33693  csbxpgVD  33694  csbrngVD  33696  csbunigVD  33698  csbfv12gALTVD  33699  bj-cleq  34519 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452
 Copyright terms: Public domain W3C validator