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

Theorem rabbidv 3220
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 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rabbidva 3219 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-rab 2950
This theorem is referenced by:  rabeqbidv  3226  difeq2  3755  seex  5106  mptiniseg  5667  dfpred3g  5729  elovmpt2rab  6922  elovmpt3rab1  6935  fineqvlem  8215  mapfien2  8355  supeq1  8392  supeq2  8395  supeq3  8396  oieq1  8458  oieq2  8459  ordtypecbv  8463  ordtypelem3  8466  harval  8508  inf3lema  8559  wemapwe  8632  oef1o  8633  tz9.12lem3  8690  rankvalb  8698  rankvalg  8718  ranksnb  8728  rankonidlem  8729  cardval3  8816  cardidm  8823  alephsuc2  8941  coftr  9133  fin1a2lem11  9270  fin1a2lem12  9271  hsmex  9292  axdc3lem2  9311  zorn2lem1  9356  zorn2lem6  9361  zorn2lem7  9362  zorn2g  9363  wuncval  9602  tskmval  9699  peano5uzti  11505  uzval  11727  rpnnen1  11858  ixxval  12221  fzval  12366  hashbclem  13274  hashbc  13275  shftfn  13857  bitsfval  15192  sadfval  15221  sadcom  15232  smufval  15246  smupp1  15249  smupval  15257  smumullem  15261  gcdval  15265  bezoutlem2  15304  bezoutlem4  15306  lcmval  15352  lcmfval  15381  lcmf0val  15382  lcmfpr  15387  isprm  15434  odzval  15543  pcval  15596  pceulem  15597  pceu  15598  pczpre  15599  pcdiv  15604  prmreclem1  15667  prmreclem4  15670  prmreclem5  15671  ramval  15759  cshws0  15855  imasdsval  16222  mrcval  16317  eldmcoa  16762  cycsubg2  17678  cntzval  17800  cntzsnval  17803  odfval  17998  odval  17999  gexval  18039  efgsfo  18198  dprdval  18448  ablfac1a  18514  ablfac1b  18515  ablfac1eu  18518  ablfaclem1  18530  ablfaclem3  18532  lspval  19023  aspval  19376  psrass1lem  19425  psrmulval  19434  mplmonmul  19512  coe1mul2  19687  ocvval  20059  dsmmelbas  20131  frlmsslss  20161  pmatcoe1fsupp  20554  istopon  20765  toponsspwpw  20774  clsval  20889  neival  20954  ordtbaslem  21040  ordtbas2  21043  ordtopn1  21046  ordtopn2  21047  cnpval  21088  llyeq  21321  nllyeq  21322  ptfinfin  21370  finlocfin  21371  dissnlocfin  21380  locfindis  21381  xkoopn  21440  kqfval  21574  tsmsfbas  21978  blvalps  22237  blval  22238  nmofval  22565  nmoval  22566  ishtpy  22818  minveclem3b  23245  minveclem3  23246  minveclem4  23249  minveclem5  23250  ovolval  23288  vitalilem2  23423  vitalilem3  23424  vitalilem4  23425  vitali  23427  itg2monolem1  23562  elcpn  23742  mdegmullem  23883  elqaalem1  24119  elqaalem2  24120  elqaalem3  24121  elqaa  24122  aannenlem1  24128  aannenlem2  24129  jensen  24760  vmaval  24884  muval  24903  sgmval  24913  fsumdvdscom  24956  musum  24962  muinv  24964  dchrisum0fval  25239  dchrisum0ff  25241  logsqvma2  25277  pntrlog2bndlem1  25311  tglngval  25491  ttgval  25800  ttgitvval  25807  ebtwntg  25907  numedglnl  26084  dfnbgr2  26275  dfnbgr3  26276  uvtxusgr  26353  vtxdgval  26420  rusgrnumwrdl2  26538  iswwlksnon  26802  iswwlksnonOLD  26803  rusgrnumwwlks  26941  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwwlknon  27063  clwwlknonOLD  27064  clwwlk0on0  27067  clwwlknondisjOLD  27090  eupth2  27217  fusgreg2wsplem  27313  fusgreghash2wsp  27318  numclwwlk3lemOLD  27369  sspval  27706  ubthlem1  27854  ubthlem2  27855  ubthlem3  27856  ocval  28267  spanval  28320  chsupid  28399  eigvecval  28883  specval  28885  iunpreima  29509  crefeq  30040  ordtcnvNEW  30094  ordtrest2NEW  30097  ordtconnlem1  30098  measvuni  30405  brfae  30439  omsfval  30484  orvcelval  30658  ballotlemi  30690  bnj602  31111  subfacp1lem6  31293  kur14  31324  cvmscbv  31366  cvmsi  31373  cvmsval  31374  snmlval  31439  snmlflim  31440  scutval  32036  fvray  32373  fwddifnval  32395  neibastop3  32482  icoreval  33331  fin2so  33526  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem32  33571  ftc1anclem6  33620  islinei  35344  pmapval  35361  paddval  35402  paddcom  35417  pclvalN  35494  ldilset  35713  dilsetN  35758  diafval  36637  diaval  36638  docavalN  36729  dicfval  36781  dochfval  36956  dochval  36957  mapdval  37234  mapdsn2  37248  2rexfrabdioph  37677  3rexfrabdioph  37678  4rexfrabdioph  37679  6rexfrabdioph  37680  7rexfrabdioph  37681  eldioph4i  37693  diophren  37694  pell1qrval  37727  pell14qrval  37729  pell1234qrval  37731  rpnnen3  37916  fnwe2lem1  37937  pwssplit4  37976  pwslnmlem2  37980  dgraaval  38031  itgoval  38048  rgspnval  38055  proot1hash  38095  rfovfvd  38613  rfovfvfvd  38614  rfovcnvf1od  38615  fsovrfovd  38620  fsovfvd  38621  fsovfvfvd  38622  fsovcnvlem  38624  nzss  38833  supminfxr  40007  dvnprodlem1  40479  dvnprodlem2  40480  dvnprodlem3  40481  dvnprod  40482  stoweidlem26  40561  stoweidlem27  40562  stoweidlem31  40566  stoweidlem34  40569  stoweidlem46  40581  fourierdlem79  40720  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem105  40746  fourierdlem107  40748  fourierdlem108  40749  fourierdlem110  40751  etransclem11  40780  salgenval  40859  subsaliuncl  40894  ovnval  41076  ovnval2  41080  ovnval2b  41087  ovncvrrp  41099  ovnsubaddlem1  41105  ovnsubadd  41107  ovncvr2  41146  hspmbl  41164  ovolval2  41179  ovnovollem3  41193  salpreimagelt  41239  salpreimalegt  41241  salpreimagtge  41255  salpreimaltle  41256  issmflem  41257  issmf  41258  salpreimagtlt  41260  smfpreimalt  41261  smfpreimaltf  41266  issmfle  41275  smfpimltxr  41277  smfpreimale  41284  issmfgt  41286  smfpreimagt  41291  issmfge  41299  smflimlem3  41302  smflimlem4  41303  smflim  41306  smfpimgtxr  41309  smfpreimage  41311  fvmptrabdm  41632  prmdvdsfmtnof1  41824  rnghmval  42216  bigoval  42668
  Copyright terms: Public domain W3C validator