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

Theorem rabeqdv 3183
Description: Equality of restricted class abstractions. Deduction form of rabeq 3182. (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 3182 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
31, 2syl 17 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {crab 2911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916
This theorem is referenced by:  rabeqbidv  3184  rabeqbidva  3185  rabsnif  4233  cantnffval  8512  dfphi2  15414  mrisval  16222  coafval  16646  pmtrfval  17802  dprdval  18334  eengv  25776  incistruhgr  25887  isupgr  25892  isumgr  25902  upgrun  25925  umgrun  25927  isuspgr  25957  isusgr  25958  isuspgrop  25966  isusgrop  25967  isausgr  25969  ausgrusgrb  25970  usgrstrrepe  26037  lfuhgr1v0e  26056  usgrexmpl  26065  usgrexi  26241  cusgrsize  26254  1loopgrvd2  26302  wwlksn  26615  wspthsn  26621  iswwlksnon  26626  iswspthsnon  26627  clwwlksn  26765  mpstval  31175  pclfvalN  34690  etransclem11  39795
  Copyright terms: Public domain W3C validator