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

Theorem rabbidv 2943
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 455 . 2
32rabbidva 2942 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1687  e.wcel 1749  {crab 2698
This theorem is referenced by:  rabeqbidv  2946  difeq2  3445  seex  4654  mptiniseg  5304  fineqvlem  7486  mapfien2  7605  supeq1  7642  supeq2  7645  supeq3  7646  oieq1  7673  oieq2  7674  ordtypecbv  7678  ordtypelem3  7681  harval  7724  inf3lema  7777  wemapwe  7875  wemapweOLD  7876  oef1o  7877  oef1oOLD  7878  tz9.12lem3  7943  rankvalb  7951  rankvalg  7971  ranksnb  7981  rankonidlem  7982  cardval3  8069  cardidm  8076  alephsuc2  8197  coftr  8389  fin1a2lem11  8526  fin1a2lem12  8527  hsmex  8548  axdc3lem2  8567  zorn2lem1  8612  zorn2lem6  8617  zorn2lem7  8618  zorn2g  8619  wuncval  8855  tskmval  8952  peano5uzti  10676  uzval  10808  reexALT  10930  ixxval  11253  fzval  11383  hashbclem  12146  hashbc  12147  shftfn  12503  rpnnen  13449  bitsfval  13559  sadfval  13588  sadcom  13599  smufval  13613  smupp1  13616  smupval  13624  smumullem  13628  gcdval  13632  bezoutlem2  13663  bezoutlem4  13665  isprm  13705  isprm2lem  13710  odzval  13803  pcval  13851  pceulem  13852  pceu  13853  pczpre  13854  pcdiv  13859  prmreclem1  13917  prmreclem4  13920  prmreclem5  13921  ramval  14009  cshws0  14068  imasdsval  14393  mrcval  14488  eldmcoa  14873  cycsubg2  15655  cntzval  15776  cntzsnval  15779  odfval  15973  odval  15974  gexval  16014  efgsfo  16173  dprdval  16370  ablfac1a  16436  ablfac1b  16437  ablfac1eu  16440  ablfaclem1  16452  ablfaclem3  16454  lspval  16865  aspval  17207  psrass1lem  17262  psrmulval  17270  mplmonmul  17350  coe1mul2  17487  ocvval  17800  dsmmelbas  17872  frlmsslss  17903  istopon  18234  clsval  18345  neival  18410  ordtbaslem  18496  ordtbas2  18499  ordtopn1  18502  ordtopn2  18503  cnpval  18544  llyeq  18778  nllyeq  18779  xkoopn  18866  kqfval  19000  tsmsfbas  19402  blvalps  19660  blval  19661  nmofval  19993  nmoval  19994  ishtpy  20244  minveclem3b  20615  minveclem3  20616  minveclem4  20619  minveclem5  20620  ovolval  20657  vitalilem2  20789  vitalilem3  20790  vitalilem4  20791  vitali  20793  itg2monolem1  20928  elcpn  21108  mdegmullem  21291  elqaalem1  21526  elqaalem2  21527  elqaalem3  21528  elqaa  21529  aannenlem1  21535  aannenlem2  21536  jensen  22123  vmaval  22192  muval  22211  sgmval  22221  fsumdvdscom  22266  musum  22272  muinv  22274  dchrisum0fval  22495  dchrisum0ff  22497  logsqvma2  22533  pntrlog2bndlem1  22567  tglngval  22720  ttgval  22800  ttgitvval  22807  ebtwntg  22907  nbgraop1  23015  vdgrval  23245  eupath2  23280  sspval  23800  ubthlem1  23950  ubthlem2  23951  ubthlem3  23952  ocval  24362  spanval  24415  chsupid  24494  eigvecval  24979  specval  24981  iunpreima  25595  ordtrest2NEW  26062  ordtconlem1  26063  measvuni  26337  brfae  26373  orvcelval  26554  ballotlemi  26586  subfacp1lem6  26776  kur14  26807  cvmscbv  26850  cvmsi  26857  cvmsval  26858  snmlval  26923  snmlflim  26924  dfpred3g  27338  fvray  27874  fin2so  28087  ftc1anclem6  28143  ptfinfin  28241  finlocfin  28242  locfindis  28248  neibastop3  28254  2rexfrabdioph  28807  3rexfrabdioph  28808  4rexfrabdioph  28809  6rexfrabdioph  28810  7rexfrabdioph  28811  eldioph4i  28824  diophren  28825  pell1qrval  28860  pell14qrval  28862  pell1234qrval  28864  rpnnen3  29054  fnwe2lem1  29076  pwssplit4  29115  pwslnmlem2  29119  mapfien2OLD  29122  dgraaval  29174  itgoval  29191  rgspnval  29198  proot1hash  29241  stoweidlem26  29495  stoweidlem27  29496  stoweidlem31  29500  stoweidlem34  29503  stoweidlem46  29515  elovmpt2rab  29832  elovmpt3rab1  29837  wwlkn  29990  2wlkonot  30058  2spthonot  30059  clwwlkn  30104  hashecclwwlkn1  30182  usghashecclwwlk  30183  rusgraprop4  30230  rusgrasn  30231  rusgranumwlkl1lem1  30232  rusgranumwlklem1  30241  rusgranumwlklem3  30243  rusgranumwlks  30248  rusgranumwlkg  30250  usg2spot2nb  30332  usgreg2spot  30334  2spotmdisj  30335  usgreghash2spot  30336  numclwwlkdisj  30347  numclwwlk3lem  30375  numclwwlk5  30379  bnj602  31486  islinei  32821  pmapval  32838  paddval  32879  paddcom  32894  pclvalN  32971  ldilset  33190  dilsetN  33234  diafval  34113  diaval  34114  docavalN  34205  dicfval  34257  dochfval  34432  dochval  34433  mapdval  34710  mapdsn2  34724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-ral 2699  df-rab 2703
  Copyright terms: Public domain W3C validator