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

Theorem rabbidv 3163
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:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 479 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rabbidva 3162 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  {crab 2899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-ral 2900  df-rab 2904
This theorem is referenced by:  rabeqbidv  3167  difeq2  3683  seex  4990  mptiniseg  5531  dfpred3g  5593  elovmpt2rab  6755  elovmpt3rab1  6768  fineqvlem  8036  mapfien2  8174  supeq1  8211  supeq2  8214  supeq3  8215  oieq1  8277  oieq2  8278  ordtypecbv  8282  ordtypelem3  8285  harval  8327  inf3lema  8381  wemapwe  8454  oef1o  8455  tz9.12lem3  8512  rankvalb  8520  rankvalg  8540  ranksnb  8550  rankonidlem  8551  cardval3  8638  cardidm  8645  alephsuc2  8763  coftr  8955  fin1a2lem11  9092  fin1a2lem12  9093  hsmex  9114  axdc3lem2  9133  zorn2lem1  9178  zorn2lem6  9183  zorn2lem7  9184  zorn2g  9185  wuncval  9420  tskmval  9517  peano5uzti  11301  uzval  11523  rpnnen1  11654  ixxval  12012  fzval  12156  hashbclem  13047  hashbc  13048  shftfn  13609  bitsfval  14931  sadfval  14960  sadcom  14971  smufval  14985  smupp1  14988  smupval  14996  smumullem  15000  gcdval  15004  bezoutlem2  15043  bezoutlem4  15045  lcmval  15091  lcmfval  15120  lcmf0val  15121  lcmfpr  15126  isprm  15173  isprm2lem  15180  odzval  15282  pcval  15335  pceulem  15336  pceu  15337  pczpre  15338  pcdiv  15343  prmreclem1  15406  prmreclem4  15409  prmreclem5  15410  ramval  15498  cshws0  15594  imasdsval  15946  mrcval  16041  eldmcoa  16486  cycsubg2  17402  cntzval  17525  cntzsnval  17528  odfval  17723  odval  17724  gexval  17764  efgsfo  17923  dprdval  18173  ablfac1a  18239  ablfac1b  18240  ablfac1eu  18243  ablfaclem1  18255  ablfaclem3  18257  lspval  18744  aspval  19097  psrass1lem  19146  psrmulval  19155  mplmonmul  19233  coe1mul2  19408  ocvval  19777  dsmmelbas  19849  frlmsslss  19879  pmatcoe1fsupp  20272  istopon  20487  clsval  20598  neival  20663  ordtbaslem  20749  ordtbas2  20752  ordtopn1  20755  ordtopn2  20756  cnpval  20797  llyeq  21030  nllyeq  21031  ptfinfin  21079  finlocfin  21080  dissnlocfin  21089  locfindis  21090  xkoopn  21149  kqfval  21283  tsmsfbas  21688  blvalps  21947  blval  21948  nmofval  22275  nmoval  22276  ishtpy  22526  minveclem3b  22951  minveclem3  22952  minveclem4  22955  minveclem5  22956  ovolval  22993  vitalilem2  23128  vitalilem3  23129  vitalilem4  23130  vitali  23132  itg2monolem1  23267  elcpn  23447  mdegmullem  23586  elqaalem1  23822  elqaalem2  23823  elqaalem3  23824  elqaa  23825  aannenlem1  23831  aannenlem2  23832  jensen  24459  vmaval  24583  muval  24602  sgmval  24612  fsumdvdscom  24655  musum  24661  muinv  24663  dchrisum0fval  24938  dchrisum0ff  24940  logsqvma2  24976  pntrlog2bndlem1  25010  tglngval  25191  ttgval  25500  ttgitvval  25507  ebtwntg  25607  nbgraopALT  25746  nbgraop1  25747  wwlkn  26003  clwwlkn  26088  hashecclwwlkn1  26154  usghashecclwwlk  26155  2wlkonot  26185  2spthonot  26186  2pthwlkonot  26205  vdgrval  26216  rusgraprop4  26264  rusgrasn  26265  rusgranumwwlkl1  26266  rusgranumwlklem1  26269  rusgranumwlklem3  26271  rusgranumwlks  26276  rusgranumwlkg  26278  eupath2  26300  usg2spot2nb  26385  usgreg2spot  26387  2spotmdisj  26388  usgreghash2spot  26389  numclwwlkun  26399  numclwwlkdisj  26400  numclwwlk3lem  26428  numclwwlk5  26432  sspval  26755  ubthlem1  26903  ubthlem2  26904  ubthlem3  26905  ocval  27316  spanval  27369  chsupid  27448  eigvecval  27932  specval  27934  iunpreima  28558  aciunf1  28638  crefeq  29033  ordtcnvNEW  29087  ordtrest2NEW  29090  ordtconlem1  29091  measvuni  29397  brfae  29431  omsfval  29476  orvcelval  29650  ballotlemi  29682  bnj602  30032  subfacp1lem6  30214  kur14  30245  cvmscbv  30287  cvmsi  30294  cvmsval  30295  snmlval  30360  snmlflim  30361  fvray  31211  fwddifnval  31233  neibastop3  31320  bj-toponss  32024  icoreval  32160  fin2so  32349  poimirlem26  32388  poimirlem27  32389  poimirlem28  32390  poimirlem32  32394  ftc1anclem6  32443  islinei  33827  pmapval  33844  paddval  33885  paddcom  33900  pclvalN  33977  ldilset  34196  dilsetN  34241  diafval  35121  diaval  35122  docavalN  35213  dicfval  35265  dochfval  35440  dochval  35441  mapdval  35718  mapdsn2  35732  2rexfrabdioph  36161  3rexfrabdioph  36162  4rexfrabdioph  36163  6rexfrabdioph  36164  7rexfrabdioph  36165  eldioph4i  36177  diophren  36178  pell1qrval  36211  pell14qrval  36213  pell1234qrval  36215  rpnnen3  36400  fnwe2lem1  36421  pwssplit4  36460  pwslnmlem2  36464  dgraaval  36516  itgoval  36533  rgspnval  36540  proot1hash  36580  rfovfvd  37099  rfovfvfvd  37100  rfovcnvf1od  37101  fsovrfovd  37106  fsovfvd  37107  fsovfvfvd  37108  fsovcnvlem  37110  nzss  37321  dvnprodlem1  38619  dvnprodlem2  38620  dvnprodlem3  38621  dvnprod  38622  stoweidlem26  38702  stoweidlem27  38703  stoweidlem31  38707  stoweidlem34  38710  stoweidlem46  38722  fourierdlem79  38861  fourierdlem96  38878  fourierdlem97  38879  fourierdlem98  38880  fourierdlem99  38881  fourierdlem105  38887  fourierdlem107  38889  fourierdlem108  38890  fourierdlem110  38892  etransclem11  38921  salgenval  39000  subsaliuncl  39035  ovnval  39214  ovnval2  39218  ovnval2b  39225  ovncvrrp  39237  ovnsubaddlem1  39243  ovnsubadd  39245  ovncvr2  39284  hspmbl  39302  ovolval2  39317  ovnovollem3  39331  salpreimagelt  39378  salpreimalegt  39380  salpreimagtge  39394  salpreimaltle  39395  issmflem  39396  issmf  39397  salpreimagtlt  39399  smfpreimalt  39400  smfpreimaltf  39406  issmfle  39415  smfpimltxr  39417  smfpreimale  39424  issmfgt  39426  smfpreimagt  39431  issmfge  39439  smflimlem3  39442  smflimlem4  39443  smflim  39446  smfpimgtxr  39449  smfpreimage  39451  prmdvdsfmtnof1  39821  dfnbgr2  40542  dfnbgr3  40543  uvtxusgr  40610  vtxdgval  40665  rusgrnumwrdl2  40767  iswwlksnon  41032  wwlks2onv  41139  rusgrnumwwlks  41158  hashecclwwlksn1  41242  umgrhashecclwwlk  41243  clwwlksndisj  41261  eupth2  41388  fusgr2wsp2nb  41479  fusgreg2wsp  41481  2wspmdisj  41482  fusgreghash2wsp  41483  av-numclwwlk3lem  41519  av-numclwwlk5  41523  rnghmval  41662  bigoval  42122
  Copyright terms: Public domain W3C validator