Theorem rabeqdv 3448

Description: Equality of restricted class abstractions. Deduction form of rabeq 3447. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypothesis

Ref	Expression
rabeqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rabeqdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rabeqdv

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

Syntax hints:   → wi 4   = wceq 1536  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433

This theorem is referenced by:  rabeqbidvaOLD  3450  rabsnif  4727  fvmptrabfv  7047  suppvalfng  8190  suppvalfn  8191  suppsnop  8201  fnsuppres  8214  pmvalg  8875  cantnffval  9700  hashbc  14488  elovmpowrd  14592  dfphi2  16807  mrisval  17674  coafval  18117  mndpsuppss  18790  pmtrfval  19482  dprdval  20037  rrgval  20713  lspfval  20988  lsppropd  21034  dsmmbas2  21774  frlmbas  21792  aspval  21910  mvrfval  22018  mhpfval  22159  psdffval  22178  clsfval  23048  ordtrest  23225  ordtrest2lem  23226  ordtrest2  23227  xkoval  23610  xkopt  23678  tsmsval2  24153  cncfval  24927  isphtpy  25026  cfilfval  25311  iscmet  25331  leftval  27916  rightval  27917  ttgval  28897  ttgvalOLD  28898  eengv  29008  isupgr  29115  upgrop  29125  isumgr  29126  upgrun  29149  umgrun  29151  isuspgr  29183  isusgr  29184  isuspgrop  29192  isusgrop  29193  isausgr  29195  ausgrusgrb  29196  usgrstrrepe  29266  lfuhgr1v0e  29285  usgrexi  29472  cusgrsize  29486  1loopgrvd2  29535  wwlksn  29866  wspthsn  29877  iswwlksnon  29882  iswspthsnon  29885  clwwlknonmpo  30117  clwwlknon  30118  clwwlk0on0  30120  rmfsupp2  33227  idlsrgval  33510  rspectopn  33827  zar0ring  33838  ordtprsval  33878  snmlfval  35314  mpstval  35519  pclfvalN  39871  docaffvalN  41103  docafvalN  41104  isprimroot  42074  dvnprodlem1  45901  etransclem11  46200  issmflem  46682  issmfd  46690  cnfsmf  46695  issmflelem  46699  issmfgtlem  46710  issmfgt  46711  issmfled  46712  issmfgtd  46716  issmfgelem  46724  fvmptrabdm  47242  prprspr2  47442  stgrusgra  47861  gpgusgra  47946  assintopmap  48049  dmatALTval  48245  rrxsphere  48597