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

Theorem rabeqdv 3167
 Description: Equality of restricted class abstractions. Deduction form of rabeq 3166. (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 3166 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
31, 2syl 17 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475  {crab 2900 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905 This theorem is referenced by:  rabeqbidv  3168  rabeqbidva  3169  rabsnif  4202  cantnffval  8443  dfphi2  15317  mrisval  16113  coafval  16537  pmtrfval  17693  dprdval  18225  eengv  25659  incistruhgr  25746  isupgr  25751  isumgr  25761  upgrun  25784  umgrun  25786  isausgra  25883  usgraeq12d  25891  usgra0v  25900  usgra1v  25919  clwwlknprop  26300  mpstval  30686  pclfvalN  34193  etransclem11  39138  isuspgr  40382  isusgr  40383  isusgrop  40392  isausgr  40394  ausgrusgrb  40395  lfuhgr1v0e  40480  usgrexmpl  40487  usgrexi  40661  cusgrsize  40670  1loopgrvd2  40718  wwlksn  41040  wspthsn  41046  iswwlksnon  41051  iswspthsnon  41052  clwwlksn  41189
 Copyright terms: Public domain W3C validator