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

Theorem rabeqdv 3460
 Description: Equality of restricted class abstractions. Deduction form of rabeq 3459. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypothesis
Ref Expression
rabeqdv.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
rabeqdv (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rabeqdv
StepHypRef Expression
1 rabeqdv.1 . 2 (𝜑𝐴 = 𝐵)
2 rabeq 3459 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
31, 2syl 17 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = 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:  rabeqbidv  3461  rabeqbidva  3462  rabsnif  4633  fvmptrabfv  6781  suppvalfn  7824  suppsnop  7831  fnsuppres  7844  pmvalg  8404  cantnffval  9114  hashbc  13807  elovmpowrd  13901  dfphi2  16100  mrisval  16892  coafval  17315  pmtrfval  18569  dprdval  19116  lspfval  19736  lsppropd  19781  rrgval  20051  dsmmbas2  20424  frlmbas  20442  aspval  20557  mvrfval  20656  mhpfval  20789  clsfval  21628  ordtrest  21805  ordtrest2lem  21806  ordtrest2  21807  xkoval  22190  xkopt  22258  tsmsval2  22733  cncfval  23491  isphtpy  23584  cfilfval  23866  iscmet  23886  ttgval  26667  eengv  26771  isupgr  26875  upgrop  26885  isumgr  26886  upgrun  26909  umgrun  26911  isuspgr  26943  isusgr  26944  isuspgrop  26952  isusgrop  26953  isausgr  26955  ausgrusgrb  26956  usgrstrrepe  27023  lfuhgr1v0e  27042  usgrexmpl  27051  usgrexi  27229  cusgrsize  27242  1loopgrvd2  27291  wwlksn  27621  wspthsn  27632  iswwlksnon  27637  iswspthsnon  27640  clwwlknonmpo  27872  clwwlknon  27873  clwwlk0on0  27875  rmfsupp2  30898  idlsrgval  31027  rspectopn  31189  ordtprsval  31235  snmlfval  32651  mpstval  32856  pclfvalN  37143  docaffvalN  38375  docafvalN  38376  etransclem11  42826  issmflem  43300  issmfd  43308  cnfsmf  43313  issmflelem  43317  issmfgtlem  43328  issmfgt  43329  issmfled  43330  issmfgtd  43333  issmfgelem  43341  fvmptrabdm  43788  prprspr2  43974  assintopmap  44405  dmatALTval  44748  rrxsphere  45101
 Copyright terms: Public domain W3C validator