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

Theorem rabeqbidv 3226
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 3225 . 2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
3 rabeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rabbidv 3220 . 2 (𝜑 → {𝑥𝐵𝜓} = {𝑥𝐵𝜒})
52, 4eqtrd 2685 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  {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-nfc 2782  df-ral 2946  df-rab 2950
This theorem is referenced by:  elfvmptrab1  6344  fvmptrabfv  6348  elovmpt2rab1  6923  ovmpt3rab1  6933  suppval  7342  mpt2xopoveq  7390  supeq123d  8397  phival  15519  dfphi2  15526  hashbcval  15753  imasval  16218  ismre  16297  mrisval  16337  isacs  16359  monfval  16439  ismon  16440  monpropd  16444  natfval  16653  isnat  16654  initoval  16694  termoval  16695  gsumvalx  17317  gsumpropd  17319  gsumress  17323  ismhm  17384  issubm  17394  issubg  17641  isnsg  17670  isgim  17751  isga  17770  cntzfval  17799  isslw  18069  isirred  18745  dfrhm2  18765  isrim0  18771  issubrg  18828  abvfval  18866  lssset  18982  islmhm  19075  islmim  19110  islbs  19124  rrgval  19335  mplval  19476  mplbaspropd  19655  ocvfval  20058  isobs  20112  dsmmval  20126  islinds  20196  dmatval  20346  scmatval  20358  cpmat  20562  cldval  20875  mretopd  20944  neifval  20951  ordtval  21041  ordtbas2  21043  ordtcnv  21053  ordtrest2  21056  cnfval  21085  cnpfval  21086  kgenval  21386  xkoval  21438  dfac14  21469  qtopval  21546  qtopval2  21547  hmeofval  21609  elmptrab  21678  fgval  21721  flimval  21814  utopval  22083  ucnval  22128  iscfilu  22139  ispsmet  22156  ismet  22175  isxmet  22176  blfvalps  22235  cncfval  22738  ishtpy  22818  isphtpy  22827  om1val  22876  cfilfval  23108  caufval  23119  cpnfval  23740  uc1pval  23944  mon1pval  23946  dchrval  25004  istrkgl  25402  israg  25637  iseqlg  25792  ttgval  25800  nbgrval  26274  uvtxavalOLD  26334  vtxdgfval  26419  vtxdeqd  26429  1egrvtxdg1  26461  umgr2v2evd2  26479  wwlks  26783  wwlksn  26785  wspthsn  26797  wwlksnon  26800  wspthsnon  26801  iswspthsnon  26806  iswspthsnonOLD  26807  rusgrnumwwlklem  26937  clwwlk  26951  clwwlkn  26985  clwwlknOLD  26986  2clwwlk  27335  numclwwlkovgOLD  27339  numclwwlkovh0  27352  numclwwlkovq  27354  numclwwlkovhOLD  27362  lnoval  27735  bloval  27764  hmoval  27793  ordtprsuni  30093  sigagenval  30331  faeval  30437  ismbfm  30442  carsgval  30493  sitgval  30522  reprval  30816  erdszelem3  31301  erdsze  31310  kur14  31324  iscvm  31367  wlimeq12  31889  fwddifval  32394  poimirlem28  33567  istotbnd  33698  isbnd  33709  rngohomval  33893  rngoisoval  33906  idlval  33942  pridlval  33962  maxidlval  33968  igenval  33990  lshpset  34583  lflset  34664  pats  34890  llnset  35109  lplnset  35133  lvolset  35176  lineset  35342  pmapfval  35360  paddfval  35401  lhpset  35599  ldilfset  35712  ltrnfset  35721  ltrnset  35722  dilfsetN  35757  trnfsetN  35760  trnsetN  35761  diaffval  36636  diafval  36637  dicffval  36780  dochffval  36955  lpolsetN  37088  lcdfval  37194  lcdval  37195  mapdffval  37232  mapdfval  37233  isnacs  37584  mzpclval  37605  issdrg  38084  k0004val  38765  fourierdlem2  40644  fourierdlem3  40645  etransclem12  40781  etransclem33  40802  caragenval  41028  smflimlem3  41302  fvmptrab  41631  iccpval  41676  ismgmhm  42108  issubmgm  42114  assintopval  42166  rnghmval  42216  isrngisom  42221  dmatALTval  42514  lcoop  42525
  Copyright terms: Public domain W3C validator