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

Theorem rabbi 3005
 Description: Equivalent wff's correspond to equal restricted class abstractions. Closed theorem form of rabbidva 3069. (Contributed by NM, 25-Nov-2013.)
Assertion
Ref Expression
rabbi

Proof of Theorem rabbi
StepHypRef Expression
1 abbi 2551 . 2
2 df-ral 2778 . . 3
3 pm5.32 640 . . . 4
43albii 1687 . . 3
52, 4bitri 252 . 2
6 df-rab 2782 . . 3
7 df-rab 2782 . . 3
86, 7eqeq12i 2440 . 2
91, 5, 83bitr4i 280 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370  wal 1435   wceq 1437   wcel 1867  cab 2405  wral 2773  crab 2777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398 This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-ral 2778  df-rab 2782 This theorem is referenced by:  rabbidva  3069  kqfeq  20676  isr0  20689  bj-rabbida  31312  rabeq12f  32148  eq0rabdioph  35372  eqrabdioph  35373  lerabdioph  35401  eluzrabdioph  35402  ltrabdioph  35404  nerabdioph  35405  dvdsrabdioph  35406  undisjrab  36339  ioodvbdlimc1lem2  37424  ioodvbdlimc2lem  37426  fourierdlem89  37675  fourierdlem91  37677  fourierdlem100  37686  fourierdlem108  37694  fourierdlem112  37698
 Copyright terms: Public domain W3C validator