Theorem rabeqdv 3430

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416

This theorem is used by:  rabeqbidvaOLD  3432  rabsnif  4688  fvmptrabfv  7022  suppvalfng  8161  suppvalfn  8162  suppsnop  8172  fnsuppres  8185  pmvalg  8832  cantnffval  9630  hashbc  14497  elovmpowrd  14602  dfphi2  16839  mrisval  17692  coafval  18127  mndpsuppss  18829  pmtrfval  19526  dprdval  20081  rrgval  20807  lspfval  21105  lsppropd  21150  rspvalint  21380  dsmmbas2  21898  frlmbas  21916  aspval  22033  mvrfval  22141  mhpfval  22312  psdffval  22331  clsfval  23193  ordtrest  23370  ordtrest2lem  23371  ordtrest2  23372  xkoval  23755  xkopt  23823  tsmsval2  24298  cncfval  25058  isphtpy  25151  cfilfval  25434  iscmet  25454  leftval  28053  rightval  28054  ttgval  29235  eengv  29340  isupgr  29445  upgrop  29455  isumgr  29456  upgrun  29479  umgrun  29481  isuspgr  29513  isusgr  29514  isuspgrop  29522  isusgrop  29523  isausgr  29525  ausgrusgrb  29526  usgrstrrepe  29596  lfuhgr1v0e  29615  usgrexi  29802  cusgrsize  29815  1loopgrvd2  29864  wwlksn  30197  wspthsn  30208  iswwlksnon  30213  iswspthsnon  30216  clwwlknonmpo  30451  clwwlknon  30452  clwwlk0on0  30454  fxpgaval  33496  rmfsupp2  33566  idlsrgval  33802  extvval  33930  splyval  33958  esplyval  33961  rspectopn  34266  zar0ring  34277  ordtprsval  34317  snmlfval  35830  mpstval  36035  pclfvalN  40691  docaffvalN  41923  docafvalN  41924  isprimroot  42888  dvnprodlem1  46688  etransclem11  46987  issmflem  47469  issmfd  47477  cnfsmf  47482  issmflelem  47486  issmfgtlem  47497  issmfgt  47498  issmfled  47499  issmfgtd  47503  issmfgelem  47511  fvmptrabdm  48058  prprspr2  48295  stgrusgra  48752  gpgusgra  48850  assintopmap  48999  dmatALTval  49208  rrxsphere  49556  initopropdlem  50046  termopropdlem  50047