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

Theorem rabbidv 3413
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rabbidv (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 481 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rabbidva 3412 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  {crab 3405
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-rab 3406
This theorem is referenced by:  difeq2  4074  seex  5592  mptiniseg  6187  dfpred3g  6261  elovmporab  7589  elovmpt3rab1  7603  fineqvlem  9139  mapfien2  9278  supeq1  9314  supeq2  9317  supeq3  9318  oieq1  9381  oieq2  9382  ordtypecbv  9386  ordtypelem3  9389  harval  9429  inf3lema  9493  wemapwe  9566  oef1o  9567  tz9.12lem3  9658  rankvalb  9666  rankvalg  9686  ranksnb  9696  rankonidlem  9697  cardval3  9821  cardidm  9828  alephsuc2  9949  coftr  10142  fin1a2lem11  10279  fin1a2lem12  10280  hsmex  10301  axdc3lem2  10320  zorn2lem1  10365  zorn2lem6  10370  zorn2lem7  10371  zorn2g  10372  wuncval  10611  tskmval  10708  peano5uzti  12523  uzval  12697  rpnnen1  12836  ixxval  13200  fzval  13354  hashbclem  14276  hashbc  14277  shftfn  14891  bitsfval  16237  sadfval  16266  sadcom  16277  smufval  16291  smupp1  16294  smupval  16302  smumullem  16306  gcdval  16310  bezoutlem2  16355  bezoutlem4  16357  lcmval  16402  lcmfval  16431  lcmf0val  16432  lcmfpr  16437  isprm  16483  odzval  16597  pcval  16650  pceulem  16651  pceu  16652  pczpre  16653  pcdiv  16658  prmreclem1  16722  prmreclem4  16725  prmreclem5  16726  ramval  16814  cshws0  16908  imasdsval  17331  mrcval  17424  eldmcoa  17885  cycsubg2  18935  cntzval  19033  cntzsnval  19036  odfval  19246  odfvalALT  19247  odval  19248  gexval  19289  efgsfo  19450  dprdval  19711  ablfac1a  19777  ablfac1b  19778  ablfac1eu  19781  ablfaclem1  19793  ablfaclem3  19795  lspval  20359  ocvval  20994  dsmmelbas  21068  frlmsslss  21103  aspval  21199  psrass1lemOLD  21265  psrass1lem  21268  psrmulval  21277  mplmonmul  21359  mhpval  21452  mhpmulcl  21461  coe1mul2  21562  pmatcoe1fsupp  21972  istopon  22183  toponsspwpw  22193  clsval  22310  neival  22375  ordtbaslem  22461  ordtbas2  22464  ordtopn1  22467  ordtopn2  22468  cnpval  22509  llyeq  22743  nllyeq  22744  ptfinfin  22792  finlocfin  22793  dissnlocfin  22802  locfindis  22803  xkoopn  22862  kqfval  22996  tsmsfbas  23401  blvalps  23660  blval  23661  nmofval  24000  nmoval  24001  ishtpy  24257  minveclem3b  24714  minveclem3  24715  minveclem4  24718  minveclem5  24719  ovolval  24759  vitalilem2  24895  vitalilem3  24896  vitalilem4  24897  vitali  24899  itg2monolem1  25037  elcpn  25220  mdegmullem  25365  elqaalem1  25601  elqaalem2  25602  elqaalem3  25603  elqaa  25604  aannenlem1  25610  aannenlem2  25611  jensen  26260  vmaval  26384  muval  26403  sgmval  26413  fsumdvdscom  26456  musum  26462  muinv  26464  dchrisum0fval  26775  dchrisum0ff  26777  logsqvma2  26813  pntrlog2bndlem1  26847  scutval  27061  tglngval  27291  ttgval  27615  ttgvalOLD  27616  ttgitvval  27628  ebtwntg  27729  numedglnl  27893  dfnbgr2  28083  dfnbgr3  28084  uvtxusgr  28148  vtxdgval  28214  rusgrnumwrdl2  28332  iswwlksnon  28596  rusgrnumwwlks  28717  hashecclwwlkn1  28819  umgrhashecclwwlk  28820  clwlknf1oclwwlknlem2  28824  clwwlknon  28832  clwwlk0on0  28834  eupth2  28981  fusgreg2wsplem  29075  fusgreghash2wsp  29080  numclwlk1lem1  29111  sspval  29463  ubthlem1  29610  ubthlem2  29611  ubthlem3  29612  ocval  30020  spanval  30073  chsupid  30152  eigvecval  30636  specval  30638  iunpreima  31280  pwrssmgc  31654  nsgqusf1olem3  31986  crefeq  32199  zarcls1  32223  zarclsun  32224  zarclsiin  32225  zarclsint  32226  zarclssn  32227  zartop  32230  zartopon  32231  zart0  32233  zarmxt1  32234  zarcmp  32236  rhmpreimacnlem  32238  rhmpreimacn  32239  ordtcnvNEW  32274  ordtrest2NEW  32277  ordtconnlem1  32278  measvuni  32586  brfae  32620  omsfval  32667  orvcelval  32841  ballotlemi  32873  bnj602  33300  subfacp1lem6  33552  kur14  33583  cvmscbv  33625  cvmsi  33632  cvmsval  33633  snmlval  33698  snmlflim  33699  satfv0  33725  satfv1  33730  satfv0fun  33738  satffunlem1lem1  33769  satffunlem2lem1  33771  satfv0fvfmla0  33780  satfv1fvfmla1  33790  prv1n  33798  naddcllem  34220  naddov2  34223  naddcom  34226  naddid1  34227  naddass  34238  fvray  34621  fwddifnval  34643  neibastop3  34729  icoreval  35719  fin2so  35960  poimirlem26  35999  poimirlem27  36000  poimirlem28  36001  poimirlem32  36005  ftc1anclem6  36051  islinei  38098  pmapval  38115  paddval  38156  paddcom  38171  pclvalN  38248  ldilset  38467  dilsetN  38511  diafval  39389  diaval  39390  docavalN  39481  dicfval  39533  dochfval  39708  dochval  39709  mapdval  39986  mapdsn2  40000  prjcrvval  40835  2rexfrabdioph  40984  3rexfrabdioph  40985  4rexfrabdioph  40986  6rexfrabdioph  40987  7rexfrabdioph  40988  eldioph4i  41000  diophren  41001  pell1qrval  41034  pell14qrval  41036  pell1234qrval  41038  rpnnen3  41221  fnwe2lem1  41242  pwssplit4  41281  pwslnmlem2  41285  dgraaval  41336  itgoval  41353  rgspnval  41360  proot1hash  41392  rfovfvd  42036  rfovfvfvd  42037  rfovcnvf1od  42038  fsovrfovd  42043  fsovfvd  42044  fsovfvfvd  42045  fsovcnvlem  42047  nzss  42361  supminfxr  43456  dvnprodlem1  43940  dvnprodlem2  43941  dvnprodlem3  43942  dvnprod  43943  stoweidlem26  44020  stoweidlem27  44021  stoweidlem31  44025  stoweidlem34  44028  stoweidlem46  44040  fourierdlem79  44179  fourierdlem96  44196  fourierdlem97  44197  fourierdlem98  44198  fourierdlem99  44199  fourierdlem105  44205  fourierdlem107  44207  fourierdlem108  44208  fourierdlem110  44210  etransclem11  44239  salgenval  44315  subsaliuncl  44352  ovnval  44535  ovnval2  44539  ovnval2b  44546  ovncvrrp  44558  ovnsubaddlem1  44564  ovnsubadd  44566  ovncvr2  44605  hspmbl  44623  ovolval2  44638  ovnovollem3  44652  salpreimagelt  44701  salpreimalegt  44703  salpreimagtge  44719  salpreimaltle  44720  issmflem  44721  issmf  44722  salpreimagtlt  44724  smfpreimalt  44725  smfpreimaltf  44730  issmfle  44739  smfpimltxr  44741  smfpreimale  44748  issmfgt  44750  smfpreimagt  44756  issmfge  44764  smflimlem3  44767  smflimlem4  44768  smflim  44771  smfpimgtxr  44774  smfpreimage  44776  fvmptrabdm  45274  elsetpreimafveq  45338  prmdvdsfmtnof1  45528  fppr  45667  rnghmval  45938  bigoval  46384  line  46567  rrxline  46569  sphere  46582  line2y  46590  inpw  46652
  Copyright terms: Public domain W3C validator