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

Proof of Theorem abbi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2429 . 2
2 nfsab1 2425 . . . 4
3 nfsab1 2425 . . . 4
42, 3nfbi 1856 . . 3
5 nfv 1629 . . 3
6 df-clab 2422 . . . . 5
7 sbequ12r 1945 . . . . 5
86, 7syl5bb 249 . . . 4
9 df-clab 2422 . . . . 5
10 sbequ12r 1945 . . . . 5
119, 10syl5bb 249 . . . 4
128, 11bibi12d 313 . . 3
134, 5, 12cbval 1982 . 2
141, 13bitr2i 242 1
 Colors of variables: wff set class Syntax hints:   wb 177  wal 1549   wceq 1652  wsb 1658   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