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

Theorem rabeqbidv 3483
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 3482 . 2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
3 rabeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rabbidv 3478 . 2 (𝜑 → {𝑥𝐵𝜓} = {𝑥𝐵𝜒})
52, 4eqtrd 2853 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  {crab 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-rab 3144
This theorem is referenced by:  elfvmptrab1w  6786  elfvmptrab1  6787  fvmptrabfv  6791  elovmporab1w  7381  elovmporab1  7382  ovmpt3rab1  7392  suppval  7821  mpoxopoveq  7874  supeq123d  8902  phival  16092  dfphi2  16099  hashbcval  16326  imasval  16772  ismre  16849  mrisval  16889  isacs  16910  monfval  16990  ismon  16991  monpropd  16995  natfval  17204  isnat  17205  initoval  17245  termoval  17246  gsumvalx  17874  gsumpropd  17876  gsumress  17880  ismhm  17946  issubm  17956  issubg  18217  isnsg  18245  isgim  18340  isga  18359  cntzfval  18388  isslw  18662  isirred  19378  dfrhm2  19398  isrim0  19404  issubrg  19464  issdrg  19503  abvfval  19518  lssset  19634  islmhm  19728  islmim  19763  islbs  19777  rrgval  19988  mplval  20136  mhpfval  20260  mplbaspropd  20333  ocvfval  20738  isobs  20792  dsmmval  20806  islinds  20881  dmatval  21029  scmatval  21041  cpmat  21245  cldval  21559  mretopd  21628  neifval  21635  ordtval  21725  ordtbas2  21727  ordtcnv  21737  ordtrest2  21740  cnfval  21769  cnpfval  21770  kgenval  22071  xkoval  22123  dfac14  22154  qtopval  22231  qtopval2  22232  hmeofval  22294  elmptrab  22363  fgval  22406  flimval  22499  utopval  22768  ucnval  22813  iscfilu  22824  ispsmet  22841  ismet  22860  isxmet  22861  blfvalps  22920  cncfval  23423  ishtpy  23503  isphtpy  23512  om1val  23561  cfilfval  23794  caufval  23805  cpnfval  24456  uc1pval  24660  mon1pval  24662  dchrval  25737  istrkgl  26171  israg  26410  iseqlg  26580  ttgval  26588  nbgrval  27045  vtxdgfval  27176  vtxdeqd  27186  1egrvtxdg1  27218  umgr2v2evd2  27236  wwlks  27540  wwlksn  27542  wspthsn  27553  wwlksnon  27556  wspthsnon  27557  iswspthsnon  27561  rusgrnumwwlklem  27676  clwwlk  27688  clwwlkn  27731  2clwwlk  28053  numclwlk1lem2  28076  numclwwlkovh0  28078  numclwwlkovq  28080  lnoval  28456  bloval  28485  hmoval  28514  tocycval  30677  prmidlval  30873  ordtprsuni  31061  sigagenval  31298  faeval  31404  ismbfm  31409  carsgval  31460  sitgval  31489  reprval  31780  erdszelem3  32337  erdsze  32346  kur14  32360  iscvm  32403  satf  32497  wlimeq12  33003  fwddifval  33520  poimirlem28  34801  istotbnd  34928  isbnd  34939  rngohomval  35123  rngoisoval  35136  idlval  35172  pridlval  35192  maxidlval  35198  igenval  35220  lshpset  35994  lflset  36075  pats  36301  llnset  36521  lplnset  36545  lvolset  36588  lineset  36754  pmapfval  36772  paddfval  36813  lhpset  37011  ldilfset  37124  ltrnfset  37133  ltrnset  37134  dilfsetN  37168  trnfsetN  37171  trnsetN  37172  diaffval  38046  diafval  38047  dicffval  38190  dochffval  38365  lpolsetN  38498  lcdfval  38604  lcdval  38605  mapdffval  38642  mapdfval  38643  isnacs  39179  mzpclval  39200  k0004val  40378  fourierdlem2  42271  fourierdlem3  42272  etransclem12  42408  etransclem33  42429  caragenval  42652  smflimlem3  42926  fvmptrab  43368  iccpval  43452  ismgmhm  43927  issubmgm  43933  assintopval  44040  rnghmval  44090  isrngisom  44095  dmatALTval  44383  lcoop  44394  lines  44646  rrxlines  44648  spheres  44661
  Copyright terms: Public domain W3C validator