Theorem rabeqdv 3431

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

Syntax hints:   → wi 4   = wceq 1540  {crab 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416

This theorem is referenced by:  rabeqbidvaOLD  3433  rabsnif  4699  fvmptrabfv  7018  suppvalfng  8166  suppvalfn  8167  suppsnop  8177  fnsuppres  8190  pmvalg  8851  cantnffval  9677  hashbc  14471  elovmpowrd  14576  dfphi2  16793  mrisval  17642  coafval  18077  mndpsuppss  18743  pmtrfval  19431  dprdval  19986  rrgval  20657  lspfval  20930  lsppropd  20976  dsmmbas2  21697  frlmbas  21715  aspval  21833  mvrfval  21941  mhpfval  22076  psdffval  22095  clsfval  22963  ordtrest  23140  ordtrest2lem  23141  ordtrest2  23142  xkoval  23525  xkopt  23593  tsmsval2  24068  cncfval  24832  isphtpy  24931  cfilfval  25216  iscmet  25236  leftval  27823  rightval  27824  ttgval  28854  eengv  28958  isupgr  29063  upgrop  29073  isumgr  29074  upgrun  29097  umgrun  29099  isuspgr  29131  isusgr  29132  isuspgrop  29140  isusgrop  29141  isausgr  29143  ausgrusgrb  29144  usgrstrrepe  29214  lfuhgr1v0e  29233  usgrexi  29420  cusgrsize  29434  1loopgrvd2  29483  wwlksn  29819  wspthsn  29830  iswwlksnon  29835  iswspthsnon  29838  clwwlknonmpo  30070  clwwlknon  30071  clwwlk0on0  30073  rmfsupp2  33233  idlsrgval  33518  rspectopn  33898  zar0ring  33909  ordtprsval  33949  snmlfval  35352  mpstval  35557  pclfvalN  39908  docaffvalN  41140  docafvalN  41141  isprimroot  42106  dvnprodlem1  45975  etransclem11  46274  issmflem  46756  issmfd  46764  cnfsmf  46769  issmflelem  46773  issmfgtlem  46784  issmfgt  46785  issmfled  46786  issmfgtd  46790  issmfgelem  46798  fvmptrabdm  47322  prprspr2  47532  stgrusgra  47971  gpgusgra  48061  assintopmap  48181  dmatALTval  48376  rrxsphere  48728  initopropdlem  49157  termopropdlem  49158