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

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

Proof of Theorem rabeqdv
StepHypRef Expression
1 rabeqdv.1 . 2 (𝜑𝐴 = 𝐵)
2 rabeq 3223 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
31, 2syl 17 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = 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-rab 2950
This theorem is referenced by:  rabeqbidv  3226  rabeqbidva  3227  rabsnif  4290  fvmptrabfv  6348  cantnffval  8598  dfphi2  15526  mrisval  16337  coafval  16761  pmtrfval  17916  dprdval  18448  eengv  25904  incistruhgr  26019  isupgr  26024  upgrop  26034  isumgr  26035  upgrun  26058  umgrun  26060  isuspgr  26092  isusgr  26093  isuspgrop  26101  isusgrop  26102  isausgr  26104  ausgrusgrb  26105  usgrstrrepe  26172  lfuhgr1v0e  26191  usgrexmpl  26200  usgrexi  26393  cusgrsize  26406  1loopgrvd2  26455  wwlksn  26785  wspthsn  26797  iswwlksnon  26802  iswwlksnonOLD  26803  iswspthsnon  26806  iswspthsnonOLD  26807  clwwlknOLD  26986  clwwlknonmpt2  27062  clwwlknon  27063  clwwlknonOLD  27064  clwwlk0on0  27067  mpstval  31558  pclfvalN  35493  etransclem11  40780  fvmptrabdm  41632
  Copyright terms: Public domain W3C validator