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

Theorem rabid2 3035
Description: An "identity" law for restricted class abstraction. (Contributed by NM, 9-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
rabid2
Distinct variable group:   ,

Proof of Theorem rabid2
StepHypRef Expression
1 abeq2 2581 . . 3
2 pm4.71 630 . . . 4
32albii 1640 . . 3
41, 3bitr4i 252 . 2
5 df-rab 2816 . . 3
65eqeq2i 2475 . 2
7 df-ral 2812 . 2
84, 6, 73bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442  A.wral 2807  {crab 2811
This theorem is referenced by:  rabxm  3808  iinrab2  4393  riinrab  4406  class2seteq  4620  dmmptg  5509  dmmptd  5716  fneqeql  5995  fmpt  6052  zfrep6  6768  axdc2lem  8849  ioomax  11628  iccmax  11629  hashbc  12502  dfphi2  14304  phiprmpw  14306  isnsg4  16244  symggen2  16496  psgnfvalfi  16538  lssuni  17586  psr1baslem  18224  psgnghm2  18617  ocv0  18708  dsmmfi  18769  frlmfibas  18795  frlmlbs  18831  ordtrest2lem  19704  comppfsc  20033  xkouni  20100  xkoccn  20120  tsmsfbas  20626  clsocv  21690  ehlbase  21838  ovolicc2lem4  21931  itg2monolem1  22157  musum  23467  lgsquadlem2  23630  vdgr1d  24903  vdgr1b  24904  frgraregorufr0  25052  ubthlem1  25786  xrsclat  27668  ordtrest2NEWlem  27904  hasheuni  28091  measvuni  28185  imambfm  28233  subfacp1lem6  28629  conpcon  28680  cvmliftmolem2  28727  cvmlift2lem12  28759  tfisg  29284  wfisg  29289  frinsg  29325  fdc  30238  isbnd3  30280  vdioph  30713  fiphp3d  30753  phisum  31159  stirlinglem14  31869  pmap1N  35491  pol1N  35634  dia1N  36780  dihwN  37016
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  df-ral 2812  df-rab 2816
  Copyright terms: Public domain W3C validator