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

Theorem rabbidv 3073
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 3072 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1370  e.wcel 1758  {crab 2804
This theorem is referenced by:  rabeqbidv  3076  difeq2  3582  seex  4800  mptiniseg  5451  fineqvlem  7662  mapfien2  7794  supeq1  7831  supeq2  7834  supeq3  7835  oieq1  7863  oieq2  7864  ordtypecbv  7868  ordtypelem3  7871  harval  7914  inf3lema  7967  wemapwe  8065  wemapweOLD  8066  oef1o  8067  oef1oOLD  8068  tz9.12lem3  8133  rankvalb  8141  rankvalg  8161  ranksnb  8171  rankonidlem  8172  cardval3  8259  cardidm  8266  alephsuc2  8387  coftr  8579  fin1a2lem11  8716  fin1a2lem12  8717  hsmex  8738  axdc3lem2  8757  zorn2lem1  8802  zorn2lem6  8807  zorn2lem7  8808  zorn2g  8809  wuncval  9046  tskmval  9143  peano5uzti  10869  uzval  11002  reexALT  11124  ixxval  11447  fzval  11584  hashbclem  12363  hashbc  12364  shftfn  12720  rpnnen  13667  bitsfval  13777  sadfval  13806  sadcom  13817  smufval  13831  smupp1  13834  smupval  13842  smumullem  13846  gcdval  13850  bezoutlem2  13881  bezoutlem4  13883  isprm  13923  isprm2lem  13928  odzval  14021  pcval  14069  pceulem  14070  pceu  14071  pczpre  14072  pcdiv  14077  prmreclem1  14135  prmreclem4  14138  prmreclem5  14139  ramval  14227  cshws0  14286  imasdsval  14612  mrcval  14707  eldmcoa  15092  cycsubg2  15877  cntzval  15998  cntzsnval  16001  odfval  16197  odval  16198  gexval  16238  efgsfo  16397  dprdval  16660  dprdvalOLD  16662  ablfac1a  16745  ablfac1b  16746  ablfac1eu  16749  ablfaclem1  16761  ablfaclem3  16763  lspval  17232  aspval  17575  psrass1lem  17623  psrmulval  17633  mplmonmul  17720  coe1mul2  17904  ocvval  18285  dsmmelbas  18357  frlmsslss  18391  pmatcoe1fsupp  18774  istopon  18929  clsval  19040  neival  19105  ordtbaslem  19191  ordtbas2  19194  ordtopn1  19197  ordtopn2  19198  cnpval  19239  llyeq  19473  nllyeq  19474  xkoopn  19561  kqfval  19695  tsmsfbas  20097  blvalps  20359  blval  20360  nmofval  20692  nmoval  20693  ishtpy  20943  minveclem3b  21314  minveclem3  21315  minveclem4  21318  minveclem5  21319  ovolval  21356  vitalilem2  21489  vitalilem3  21490  vitalilem4  21491  vitali  21493  itg2monolem1  21628  elcpn  21808  mdegmullem  21949  elqaalem1  22185  elqaalem2  22186  elqaalem3  22187  elqaa  22188  aannenlem1  22194  aannenlem2  22195  jensen  22782  vmaval  22851  muval  22870  sgmval  22880  fsumdvdscom  22925  musum  22931  muinv  22933  dchrisum0fval  23154  dchrisum0ff  23156  logsqvma2  23192  pntrlog2bndlem1  23226  tglngval  23402  ttgval  23590  ttgitvval  23597  ebtwntg  23697  nbgraop1  23805  vdgrval  24035  eupath2  24070  sspval  24590  ubthlem1  24740  ubthlem2  24741  ubthlem3  24742  ocval  25152  spanval  25205  chsupid  25284  eigvecval  25769  specval  25771  iunpreima  26383  ordtrest2NEW  26810  ordtconlem1  26811  measvuni  27085  brfae  27120  omsfval  27165  orvcelval  27307  ballotlemi  27339  subfacp1lem6  27529  kur14  27560  cvmscbv  27603  cvmsi  27610  cvmsval  27611  snmlval  27676  snmlflim  27677  dfpred3g  28092  fvray  28628  fin2so  28876  ftc1anclem6  28932  ptfinfin  29030  finlocfin  29031  locfindis  29037  neibastop3  29043  2rexfrabdioph  29594  3rexfrabdioph  29595  4rexfrabdioph  29596  6rexfrabdioph  29597  7rexfrabdioph  29598  eldioph4i  29611  diophren  29612  pell1qrval  29647  pell14qrval  29649  pell1234qrval  29651  rpnnen3  29841  fnwe2lem1  29863  pwssplit4  29902  pwslnmlem2  29906  mapfien2OLD  29909  dgraaval  29961  itgoval  29978  rgspnval  29985  proot1hash  30028  stoweidlem26  30555  stoweidlem27  30556  stoweidlem31  30560  stoweidlem34  30563  stoweidlem46  30575  fourierdlem79  30715  fourierdlem96  30732  fourierdlem97  30733  fourierdlem98  30734  fourierdlem99  30735  fourierdlem105  30741  fourierdlem107  30743  elovmpt2rab  31035  elovmpt3rab1  31040  wwlkn  31193  2wlkonot  31261  2spthonot  31262  clwwlkn  31307  hashecclwwlkn1  31385  usghashecclwwlk  31386  rusgraprop4  31433  rusgrasn  31434  rusgranumwlkl1lem1  31435  rusgranumwlklem1  31444  rusgranumwlklem3  31446  rusgranumwlks  31451  rusgranumwlkg  31453  usg2spot2nb  31535  usgreg2spot  31537  2spotmdisj  31538  usgreghash2spot  31539  numclwwlkdisj  31550  numclwwlk3lem  31578  numclwwlk5  31582  bnj602  32751  islinei  34235  pmapval  34252  paddval  34293  paddcom  34308  pclvalN  34385  ldilset  34604  dilsetN  34648  diafval  35527  diaval  35528  docavalN  35619  dicfval  35671  dochfval  35846  dochval  35847  mapdval  36124  mapdsn2  36138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2805  df-rab 2809
  Copyright terms: Public domain W3C validator