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

Theorem rabbidv 3101
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1
Assertion
Ref Expression
rabbidv
Distinct variable group:   ,

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3
21adantr 465 . 2
32rabbidva 3100 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818  {crab 2811
This theorem is referenced by:  rabeqbidv  3104  difeq2  3615  seex  4847  mptiniseg  5506  elovmpt2rab  6521  elovmpt3rab1  6536  fineqvlem  7754  mapfien2  7888  supeq1  7925  supeq2  7928  supeq3  7929  oieq1  7958  oieq2  7959  ordtypecbv  7963  ordtypelem3  7966  harval  8009  inf3lema  8062  wemapwe  8160  wemapweOLD  8161  oef1o  8162  oef1oOLD  8163  tz9.12lem3  8228  rankvalb  8236  rankvalg  8256  ranksnb  8266  rankonidlem  8267  cardval3  8354  cardidm  8361  alephsuc2  8482  coftr  8674  fin1a2lem11  8811  fin1a2lem12  8812  hsmex  8833  axdc3lem2  8852  zorn2lem1  8897  zorn2lem6  8902  zorn2lem7  8903  zorn2g  8904  wuncval  9141  tskmval  9238  peano5uzti  10977  uzval  11112  reexALT  11243  ixxval  11566  fzval  11703  hashbclem  12501  hashbc  12502  shftfn  12906  rpnnen  13960  bitsfval  14073  sadfval  14102  sadcom  14113  smufval  14127  smupp1  14130  smupval  14138  smumullem  14142  gcdval  14146  bezoutlem2  14177  bezoutlem4  14179  isprm  14219  isprm2lem  14224  odzval  14318  pcval  14368  pceulem  14369  pceu  14370  pczpre  14371  pcdiv  14376  prmreclem1  14434  prmreclem4  14437  prmreclem5  14438  ramval  14526  cshws0  14586  imasdsval  14912  mrcval  15007  eldmcoa  15392  cycsubg2  16238  cntzval  16359  cntzsnval  16362  odfval  16557  odval  16558  gexval  16598  efgsfo  16757  dprdval  17034  dprdvalOLD  17036  ablfac1a  17120  ablfac1b  17121  ablfac1eu  17124  ablfaclem1  17136  ablfaclem3  17138  lspval  17621  aspval  17977  psrass1lem  18029  psrmulval  18039  mplmonmul  18126  coe1mul2  18310  ocvval  18698  dsmmelbas  18770  frlmsslss  18804  pmatcoe1fsupp  19202  istopon  19426  clsval  19538  neival  19603  ordtbaslem  19689  ordtbas2  19692  ordtopn1  19695  ordtopn2  19696  cnpval  19737  llyeq  19971  nllyeq  19972  ptfinfin  20020  finlocfin  20021  dissnlocfin  20030  locfindis  20031  xkoopn  20090  kqfval  20224  tsmsfbas  20626  blvalps  20888  blval  20889  nmofval  21221  nmoval  21222  ishtpy  21472  minveclem3b  21843  minveclem3  21844  minveclem4  21847  minveclem5  21848  ovolval  21885  vitalilem2  22018  vitalilem3  22019  vitalilem4  22020  vitali  22022  itg2monolem1  22157  elcpn  22337  mdegmullem  22478  elqaalem1  22715  elqaalem2  22716  elqaalem3  22717  elqaa  22718  aannenlem1  22724  aannenlem2  22725  jensen  23318  vmaval  23387  muval  23406  sgmval  23416  fsumdvdscom  23461  musum  23467  muinv  23469  dchrisum0fval  23690  dchrisum0ff  23692  logsqvma2  23728  pntrlog2bndlem1  23762  tglngval  23938  ttgval  24178  ttgitvval  24185  ebtwntg  24285  nbgraopALT  24424  nbgraop1  24425  wwlkn  24682  clwwlkn  24767  hashecclwwlkn1  24834  usghashecclwwlk  24835  2wlkonot  24865  2spthonot  24866  2pthwlkonot  24885  vdgrval  24896  rusgraprop4  24944  rusgrasn  24945  rusgranumwwlkl1  24946  rusgranumwlklem1  24949  rusgranumwlklem3  24951  rusgranumwlks  24956  rusgranumwlkg  24958  eupath2  24980  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  usgreghash2spot  25069  numclwwlkdisj  25080  numclwwlk3lem  25108  numclwwlk5  25112  sspval  25636  ubthlem1  25786  ubthlem2  25787  ubthlem3  25788  ocval  26198  spanval  26251  chsupid  26330  eigvecval  26815  specval  26817  iunpreima  27432  crefeq  27848  ordtcnvNEW  27902  ordtrest2NEW  27905  ordtconlem1  27906  measvuni  28185  brfae  28220  omsfval  28265  orvcelval  28407  ballotlemi  28439  subfacp1lem6  28629  kur14  28660  cvmscbv  28703  cvmsi  28710  cvmsval  28711  snmlval  28776  snmlflim  28777  dfpred3g  29255  fvray  29791  fin2so  30040  ftc1anclem6  30095  neibastop3  30180  2rexfrabdioph  30729  3rexfrabdioph  30730  4rexfrabdioph  30731  6rexfrabdioph  30732  7rexfrabdioph  30733  eldioph4i  30746  diophren  30747  pell1qrval  30782  pell14qrval  30784  pell1234qrval  30786  rpnnen3  30974  fnwe2lem1  30996  pwssplit4  31035  pwslnmlem2  31039  mapfien2OLD  31042  dgraaval  31093  itgoval  31110  rgspnval  31117  proot1hash  31160  lcmval  31198  nzss  31222  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  dvnprod  31746  stoweidlem26  31808  stoweidlem27  31809  stoweidlem31  31813  stoweidlem34  31816  stoweidlem46  31828  fourierdlem79  31968  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem105  31994  fourierdlem107  31996  fourierdlem108  31997  fourierdlem110  31999  etransclem11  32028  rnghmval  32697  bnj602  33973  islinei  35464  pmapval  35481  paddval  35522  paddcom  35537  pclvalN  35614  ldilset  35833  dilsetN  35878  diafval  36758  diaval  36759  docavalN  36850  dicfval  36902  dochfval  37077  dochval  37078  mapdval  37355  mapdsn2  37369
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