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

Theorem abbi 2406
 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 2290 . 2
2 nfsab1 2286 . . . 4
3 nfsab1 2286 . . . 4
42, 3nfbi 1784 . . 3
5 nfv 1609 . . 3
6 df-clab 2283 . . . . 5
7 sbequ12r 1873 . . . . 5
86, 7syl5bb 248 . . . 4
9 df-clab 2283 . . . . 5
10 sbequ12r 1873 . . . . 5
119, 10syl5bb 248 . . . 4
128, 11bibi12d 312 . . 3
134, 5, 12cbval 1937 . 2
141, 13bitr2i 241 1
 Colors of variables: wff set class Syntax hints:   wb 176  wal 1530   wceq 1632  wsb 1638   wcel 1696  cab 2282 This theorem is referenced by:  abbii  2408  abbid  2409  rabbi  2731  dfiota2  5236  iotabi  5244  uniabio  5245  iotanul  5250  karden  7581  iuneq12daf  23170  iuneq12df  23171  rabbidva2  23180  elnev  27741  csbingVD  28976  csbsngVD  28985  csbxpgVD  28986  csbrngVD  28988  csbunigVD  28990  csbfv12gALTVD  28991 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289
 Copyright terms: Public domain W3C validator