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

Theorem rabeqbidv 3385
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 3384 . 2 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
3 rabeqbidv.2 . . 3 (𝜑 → (𝜓𝜒))
43rabbidv 3379 . 2 (𝜑 → {𝑥𝐵𝜓} = {𝑥𝐵𝜒})
52, 4eqtrd 2840 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  {crab 3100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rab 3105
This theorem is referenced by:  elfvmptrab1  6522  fvmptrabfv  6526  elovmpt2rab1  7107  ovmpt3rab1  7117  suppval  7527  mpt2xopoveq  7576  supeq123d  8591  phival  15685  dfphi2  15692  hashbcval  15919  imasval  16372  ismre  16451  mrisval  16491  isacs  16512  monfval  16592  ismon  16593  monpropd  16597  natfval  16806  isnat  16807  initoval  16847  termoval  16848  gsumvalx  17471  gsumpropd  17473  gsumress  17477  ismhm  17538  issubm  17548  issubg  17792  isnsg  17821  isgim  17902  isga  17921  cntzfval  17950  isslw  18220  isirred  18897  dfrhm2  18917  isrim0  18923  issubrg  18980  abvfval  19018  lssset  19134  islmhm  19230  islmim  19265  islbs  19279  rrgval  19492  mplval  19633  mplbaspropd  19811  ocvfval  20217  isobs  20271  dsmmval  20285  islinds  20355  dmatval  20506  scmatval  20518  cpmat  20724  cldval  21038  mretopd  21107  neifval  21114  ordtval  21204  ordtbas2  21206  ordtcnv  21216  ordtrest2  21219  cnfval  21248  cnpfval  21249  kgenval  21549  xkoval  21601  dfac14  21632  qtopval  21709  qtopval2  21710  hmeofval  21772  elmptrab  21841  fgval  21884  flimval  21977  utopval  22246  ucnval  22291  iscfilu  22302  ispsmet  22319  ismet  22338  isxmet  22339  blfvalps  22398  cncfval  22901  ishtpy  22981  isphtpy  22990  om1val  23039  cfilfval  23272  caufval  23283  cpnfval  23908  uc1pval  24112  mon1pval  24114  dchrval  25172  istrkgl  25570  israg  25805  iseqlg  25960  ttgval  25968  nbgrval  26444  uvtxavalOLD  26505  vtxdgfval  26590  vtxdeqd  26600  1egrvtxdg1  26632  umgr2v2evd2  26650  wwlks  26955  wwlksn  26957  wspthsn  26969  wwlksnon  26972  wspthsnon  26973  iswspthsnon  26978  iswspthsnonOLD  26979  rusgrnumwwlklem  27111  clwwlk  27125  clwwlkn  27170  clwwlknOLD  27171  2clwwlk  27523  numclwwlkovgOLD  27527  numclwlk1lem2  27549  numclwwlkovh0  27551  numclwwlkovq  27553  numclwwlkovhOLD  27561  lnoval  27934  bloval  27963  hmoval  27992  ordtprsuni  30289  sigagenval  30527  faeval  30633  ismbfm  30638  carsgval  30689  sitgval  30718  reprval  31012  erdszelem3  31496  erdsze  31505  kur14  31519  iscvm  31562  wlimeq12  32083  fwddifval  32588  poimirlem28  33748  istotbnd  33877  isbnd  33888  rngohomval  34072  rngoisoval  34085  idlval  34121  pridlval  34141  maxidlval  34147  igenval  34169  lshpset  34756  lflset  34837  pats  35063  llnset  35283  lplnset  35307  lvolset  35350  lineset  35516  pmapfval  35534  paddfval  35575  lhpset  35773  ldilfset  35886  ltrnfset  35895  ltrnset  35896  dilfsetN  35930  trnfsetN  35933  trnsetN  35934  diaffval  36808  diafval  36809  dicffval  36952  dochffval  37127  lpolsetN  37260  lcdfval  37366  lcdval  37367  mapdffval  37404  mapdfval  37405  isnacs  37766  mzpclval  37787  issdrg  38265  k0004val  38945  fourierdlem2  40802  fourierdlem3  40803  etransclem12  40939  etransclem33  40960  caragenval  41186  smflimlem3  41460  fvmptrab  41879  iccpval  41923  ismgmhm  42348  issubmgm  42354  assintopval  42406  rnghmval  42456  isrngisom  42461  dmatALTval  42754  lcoop  42765
  Copyright terms: Public domain W3C validator