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

Theorem rabeqbidv 3167
Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)
Hypotheses
Ref Expression
rabeqbidv.1 (𝜑𝐴 = 𝐵)
rabeqbidv.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rabeqbidv (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rabeqbidv
StepHypRef Expression
1 rabeqbidv.1 . . 3 (𝜑𝐴 = 𝐵)
21rabeqdv 3166 . 2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
3 rabeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rabbidv 3163 . 2 (𝜑 → {𝑥𝐵𝜓} = {𝑥𝐵𝜒})
52, 4eqtrd 2643 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  {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-nfc 2739  df-ral 2900  df-rab 2904
This theorem is referenced by:  elfvmptrab1  6198  elovmpt2rab1  6756  ovmpt3rab1  6766  suppval  7161  mpt2xopoveq  7209  supeq123d  8216  phival  15256  dfphi2  15263  hashbcval  15490  imasval  15940  ismre  16019  mrisval  16059  isacs  16081  monfval  16161  ismon  16162  monpropd  16166  natfval  16375  isnat  16376  initoval  16416  termoval  16417  gsumvalx  17039  gsumpropd  17041  gsumress  17045  ismhm  17106  issubm  17116  issubg  17363  isnsg  17392  isgim  17473  isga  17493  cntzfval  17522  isslw  17792  isirred  18468  dfrhm2  18486  isrim0  18492  issubrg  18549  abvfval  18587  lssset  18701  islmhm  18794  islmim  18829  islbs  18843  rrgval  19054  mplval  19195  mplbaspropd  19374  ocvfval  19771  isobs  19825  dsmmval  19839  islinds  19909  dmatval  20059  scmatval  20071  cpmat  20275  cldval  20579  mretopd  20648  neifval  20655  ordtval  20745  ordtbas2  20747  ordtcnv  20757  ordtrest2  20760  cnfval  20789  cnpfval  20790  kgenval  21090  xkoval  21142  dfac14  21173  qtopval  21250  qtopval2  21251  hmeofval  21313  elmptrab  21382  fgval  21426  flimval  21519  utopval  21788  ucnval  21833  iscfilu  21844  ispsmet  21861  ismet  21879  isxmet  21880  blfvalps  21939  cncfval  22430  ishtpy  22510  isphtpy  22519  om1val  22569  cfilfval  22788  caufval  22799  cpnfval  23418  uc1pval  23620  mon1pval  23622  dchrval  24676  istrkgl  25074  israg  25310  iseqlg  25465  ttgval  25473  nbgraop  25718  isuvtx  25782  wwlk  25975  clwwlk  26060  is2wlkonot  26156  is2spthonot  26157  2wlksot  26160  2spthsot  26161  2wlkonot3v  26168  2spthonot3v  26169  vdgrfval  26188  rusgranumwlklem2  26243  numclwwlkovf  26374  numclwwlkovg  26380  numclwwlkovq  26392  numclwwlkovh  26394  numclwwlk5  26405  lnoval  26797  bloval  26826  hmoval  26855  ordtprsuni  29099  sigagenval  29336  faeval  29442  ismbfm  29447  carsgval  29498  sitgval  29527  erdszelem3  30235  erdsze  30244  kur14  30258  iscvm  30301  wlimeq12  30815  fwddifval  31245  poimirlem28  32403  istotbnd  32534  isbnd  32545  rngohomval  32729  rngoisoval  32742  idlval  32778  pridlval  32798  maxidlval  32804  igenval  32826  lshpset  33079  lflset  33160  pats  33386  llnset  33605  lplnset  33629  lvolset  33672  lineset  33838  pmapfval  33856  paddfval  33897  lhpset  34095  ldilfset  34208  ltrnfset  34217  ltrnset  34218  dilfsetN  34253  trnfsetN  34256  trnsetN  34257  diaffval  35133  diafval  35134  dicffval  35277  dochffval  35452  lpolsetN  35585  lcdfval  35691  lcdval  35692  mapdffval  35729  mapdfval  35730  isnacs  36081  mzpclval  36102  issdrg  36582  k0004val  37264  fourierdlem2  38799  fourierdlem3  38800  etransclem12  38936  etransclem33  38957  caragenval  39180  smflimlem3  39456  iccpval  39751  nbgrval  40555  uvtxaval  40608  vtxdgfval  40678  vtxdeqd  40687  1egrvtxdg1  40720  umgr2v2evd2  40738  wwlks  41033  wwlksn  41035  wspthsn  41041  wwlksnon  41044  wspthsnon  41045  iswspthsnon  41047  rusgrnumwwlklem  41168  clwwlks  41182  clwwlksn  41184  av-numclwwlkovf  41506  av-numclwwlkovg  41513  av-numclwwlkovq  41524  av-numclwwlkovh  41526  av-numclwwlk5  41537  ismgmhm  41568  issubmgm  41574  assintopval  41626  rnghmval  41676  isrngisom  41681  dmatALTval  41978  lcoop  41989
  Copyright terms: Public domain W3C validator