Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Theorem eq2ab 2282
 Description: Equality of two class abstractions means their wff's are equivalent.
Assertion
Ref Expression
eq2ab

Proof of Theorem eq2ab
StepHypRef Expression
1 hbab1 2160 . . 3
2 hbab1 2160 . . 3
31, 2cleqf 2264 . 2
4 abid 2159 . . . 4
5 abid 2159 . . . 4
64, 5bibi12i 379 . . 3
76albii 1664 . 2
83, 7bitri 306 1
 Colors of variables: wff set class Syntax hints:   wb 231  wal 1613   wceq 1615   wcel 1617  cab 2157 This theorem is referenced by:  abbii 2284  abbid 2285  dfiota2 5260  iotabi 5268  uniabio 5269  iotanul 5272  pw2en 5714  karden 6160  grphm 16035  elnev 17489  csbingVD 17803  csbsngVD 17812  csbxpgVD 17813  csbrngVD 17815  csbunigVD 17817  csbfv12gALTVD 17818 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-10 1625  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152 This theorem depends on definitions:  df-bi 232  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166