Theorem rabeqdv 3391

Description: Equality of restricted class abstractions. Deduction form of rabeq 3389. (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 3389	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   = wceq 1601  {crab 3094

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099

This theorem is referenced by:  rabeqbidv  3392  rabeqbidva  3393  rabsnif  4490  fvmptrabfv  6571  suppvalfn  7583  fnsuppres  7604  pmvalg  8151  cantnffval  8857  hashbc  13551  elovmpt2wrd  13648  dfphi2  15883  mrisval  16676  coafval  17099  pmtrfval  18253  dprdval  18789  cncfval  23099  eengv  26328  incistruhgr  26427  isupgr  26432  upgrop  26442  isumgr  26443  upgrun  26466  umgrun  26468  isuspgr  26501  isusgr  26502  isuspgrop  26510  isusgrop  26511  isausgr  26513  ausgrusgrb  26514  usgrstrrepe  26582  lfuhgr1v0e  26601  usgrexmpl  26610  usgrexi  26789  cusgrsize  26802  1loopgrvd2  26851  wwlksn  27186  wspthsn  27197  iswwlksnon  27202  iswspthsnon  27205  clwwlknonmpt2  27491  clwwlknon  27492  clwwlk0on0  27494  mpstval  32031  pclfvalN  36045  etransclem11  41393  fvmptrabdm  42338  prprspr2  42461  rrxsphere  43488