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

Theorem rabeqbidv 3461
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 3460 . 2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
3 rabeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rabbidv 3455 . 2 (𝜑 → {𝑥𝐵𝜓} = {𝑥𝐵𝜒})
52, 4eqtrd 2857 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  {crab 3134
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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-rab 3139
This theorem is referenced by:  elfvmptrab1w  6776  elfvmptrab1  6777  fvmptrabfv  6781  elovmporab1w  7377  elovmporab1  7378  ovmpt3rab1  7388  suppval  7819  mpoxopoveq  7872  supeq123d  8902  phival  16093  dfphi2  16100  hashbcval  16327  imasval  16775  ismre  16852  mrisval  16892  isacs  16913  monfval  16993  ismon  16994  monpropd  16998  natfval  17207  isnat  17208  initoval  17248  termoval  17249  gsumvalx  17877  gsumpropd  17879  gsumress  17883  ismhm  17949  issubm  17959  issubg  18270  isnsg  18298  isgim  18393  isga  18412  cntzfval  18441  isslw  18724  isirred  19443  dfrhm2  19463  isrim0  19469  issubrg  19526  issdrg  19565  abvfval  19580  lssset  19696  islmhm  19790  islmim  19825  islbs  19839  rrgval  20051  ocvfval  20353  isobs  20407  dsmmval  20421  islinds  20496  mplval  20664  mhpfval  20789  mplbaspropd  20864  dmatval  21095  scmatval  21107  cpmat  21312  cldval  21626  mretopd  21695  neifval  21702  ordtval  21792  ordtbas2  21794  ordtcnv  21804  ordtrest2  21807  cnfval  21836  cnpfval  21837  kgenval  22138  xkoval  22190  dfac14  22221  qtopval  22298  qtopval2  22299  hmeofval  22361  elmptrab  22430  fgval  22473  flimval  22566  utopval  22836  ucnval  22881  iscfilu  22892  ispsmet  22909  ismet  22928  isxmet  22929  blfvalps  22988  cncfval  23491  ishtpy  23575  isphtpy  23584  om1val  23633  cfilfval  23866  caufval  23877  cpnfval  24533  uc1pval  24738  mon1pval  24740  dchrval  25816  istrkgl  26250  israg  26489  iseqlg  26659  ttgval  26667  nbgrval  27124  vtxdgfval  27255  vtxdeqd  27265  1egrvtxdg1  27297  umgr2v2evd2  27315  wwlks  27619  wwlksn  27621  wspthsn  27632  wwlksnon  27635  wspthsnon  27636  iswspthsnon  27640  rusgrnumwwlklem  27754  clwwlk  27766  clwwlkn  27809  2clwwlk  28130  numclwlk1lem2  28153  numclwwlkovh0  28155  numclwwlkovq  28157  lnoval  28533  bloval  28562  hmoval  28591  mntoval  30674  tocycval  30781  prmidlval  30994  mxidlval  31012  ordtprsuni  31236  sigagenval  31473  faeval  31579  ismbfm  31584  carsgval  31635  sitgval  31664  reprval  31955  erdszelem3  32514  erdsze  32523  kur14  32537  iscvm  32580  satf  32674  wlimeq12  33180  fwddifval  33697  poimirlem28  35044  istotbnd  35166  isbnd  35177  rngohomval  35361  rngoisoval  35374  idlval  35410  pridlval  35430  maxidlval  35436  igenval  35458  lshpset  36233  lflset  36314  pats  36540  llnset  36760  lplnset  36784  lvolset  36827  lineset  36993  pmapfval  37011  paddfval  37052  lhpset  37250  ldilfset  37363  ltrnfset  37372  ltrnset  37373  dilfsetN  37407  trnfsetN  37410  trnsetN  37411  diaffval  38285  diafval  38286  dicffval  38429  dochffval  38604  lpolsetN  38737  lcdfval  38843  lcdval  38844  mapdffval  38881  mapdfval  38882  isnacs  39576  mzpclval  39597  k0004val  40787  fourierdlem2  42691  fourierdlem3  42692  etransclem12  42828  etransclem33  42849  caragenval  43072  smflimlem3  43346  fvmptrab  43788  iccpval  43872  ismgmhm  44343  issubmgm  44349  assintopval  44405  rnghmval  44455  isrngisom  44460  dmatALTval  44749  lcoop  44760  lines  45085  rrxlines  45087  spheres  45100
  Copyright terms: Public domain W3C validator