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 1562  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-rab 3417

This theorem is referenced by:  rabeqbidvaOLD  3433  rabsnif  4684  fvmptrabfv  7010  suppvalfng  8149  suppvalfn  8150  suppsnop  8160  fnsuppres  8173  pmvalg  8820  cantnffval  9620  hashbc  14468  elovmpowrd  14573  dfphi2  16811  mrisval  17664  coafval  18099  mndpsuppss  18801  pmtrfval  19492  dprdval  20047  rrgval  20749  lspfval  21042  lsppropd  21087  dsmmbas2  21791  frlmbas  21809  aspval  21926  mvrfval  22034  mhpfval  22205  psdffval  22224  clsfval  23087  ordtrest  23264  ordtrest2lem  23265  ordtrest2  23266  xkoval  23649  xkopt  23717  tsmsval2  24192  cncfval  24952  isphtpy  25045  cfilfval  25328  iscmet  25348  leftval  27944  rightval  27945  ttgval  29077  eengv  29182  isupgr  29287  upgrop  29297  isumgr  29298  upgrun  29321  umgrun  29323  isuspgr  29355  isusgr  29356  isuspgrop  29364  isusgrop  29365  isausgr  29367  ausgrusgrb  29368  usgrstrrepe  29438  lfuhgr1v0e  29457  usgrexi  29644  cusgrsize  29657  1loopgrvd2  29706  wwlksn  30039  wspthsn  30050  iswwlksnon  30055  iswspthsnon  30058  clwwlknonmpo  30293  clwwlknon  30294  clwwlk0on0  30296  fxpgaval  33349  rmfsupp2  33420  idlsrgval  33701  extvval  33830  splyval  33858  esplyval  33861  rspectopn  34166  zar0ring  34177  ordtprsval  34217  snmlfval  35685  mpstval  35890  pclfvalN  40518  docaffvalN  41750  docafvalN  41751  isprimroot  42715  dvnprodlem1  46525  etransclem11  46824  issmflem  47306  issmfd  47314  cnfsmf  47319  issmflelem  47323  issmfgtlem  47334  issmfgt  47335  issmfled  47336  issmfgtd  47340  issmfgelem  47348  fvmptrabdm  47892  prprspr2  48129  stgrusgra  48586  gpgusgra  48684  assintopmap  48833  dmatALTval  49027  rrxsphere  49375  initopropdlem  49866  termopropdlem  49867