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

Step	Hyp	Ref	Expression
1		rabeqdv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeq 3223	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

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