Theorem rabeqdv 3408

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

Syntax hints:   → wi 4   = wceq 1548  {crab 3393

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394

This theorem is referenced by:  rabeqbidvaOLD  3410  rabsnif  4658  fvmptrabfv  6972  suppvalfng  8111  suppvalfn  8112  suppsnop  8122  fnsuppres  8135  pmvalg  8778  cantnffval  9579  hashbc  14410  elovmpowrd  14515  dfphi2  16739  mrisval  17591  coafval  18026  mndpsuppss  18728  pmtrfval  19420  dprdval  19975  rrgval  20673  lspfval  20967  lsppropd  21012  dsmmbas2  21716  frlmbas  21734  aspval  21851  mvrfval  21959  mhpfval  22130  psdffval  22149  clsfval  23012  ordtrest  23189  ordtrest2lem  23190  ordtrest2  23191  xkoval  23574  xkopt  23642  tsmsval2  24117  cncfval  24877  isphtpy  24970  cfilfval  25253  iscmet  25273  leftval  27863  rightval  27864  ttgval  28965  eengv  29070  isupgr  29175  upgrop  29185  isumgr  29186  upgrun  29209  umgrun  29211  isuspgr  29243  isusgr  29244  isuspgrop  29252  isusgrop  29253  isausgr  29255  ausgrusgrb  29256  usgrstrrepe  29326  lfuhgr1v0e  29345  usgrexi  29532  cusgrsize  29545  1loopgrvd2  29594  wwlksn  29927  wspthsn  29938  iswwlksnon  29943  iswspthsnon  29946  clwwlknonmpo  30181  clwwlknon  30182  clwwlk0on0  30184  fxpgaval  33252  rmfsupp2  33323  idlsrgval  33598  extvval  33727  splyval  33755  esplyval  33758  rspectopn  34063  zar0ring  34074  ordtprsval  34114  snmlfval  35573  mpstval  35778  pclfvalN  40396  docaffvalN  41628  docafvalN  41629  isprimroot  42593  dvnprodlem1  46403  etransclem11  46702  issmflem  47184  issmfd  47192  cnfsmf  47197  issmflelem  47201  issmfgtlem  47212  issmfgt  47213  issmfled  47214  issmfgtd  47218  issmfgelem  47226  fvmptrabdm  47770  prprspr2  48007  stgrusgra  48464  gpgusgra  48562  assintopmap  48711  dmatALTval  48905  rrxsphere  49253  initopropdlem  49744  termopropdlem  49745