Theorem rabeqdv 3432

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

Syntax hints:   → wi 4   = wceq 1538  {crab 3110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115

This theorem is referenced by:  rabeqbidv  3433  rabeqbidva  3434  rabsnif  4619  fvmptrabfv  6776  suppvalfn  7820  suppsnop  7827  fnsuppres  7840  pmvalg  8400  cantnffval  9110  hashbc  13807  elovmpowrd  13901  dfphi2  16101  mrisval  16893  coafval  17316  pmtrfval  18570  dprdval  19118  lspfval  19738  lsppropd  19783  rrgval  20053  dsmmbas2  20426  frlmbas  20444  aspval  20559  mvrfval  20658  mhpfval  20791  clsfval  21630  ordtrest  21807  ordtrest2lem  21808  ordtrest2  21809  xkoval  22192  xkopt  22260  tsmsval2  22735  cncfval  23493  isphtpy  23586  cfilfval  23868  iscmet  23888  ttgval  26669  eengv  26773  isupgr  26877  upgrop  26887  isumgr  26888  upgrun  26911  umgrun  26913  isuspgr  26945  isusgr  26946  isuspgrop  26954  isusgrop  26955  isausgr  26957  ausgrusgrb  26958  usgrstrrepe  27025  lfuhgr1v0e  27044  usgrexmpl  27053  usgrexi  27231  cusgrsize  27244  1loopgrvd2  27293  wwlksn  27623  wspthsn  27634  iswwlksnon  27639  iswspthsnon  27642  clwwlknonmpo  27874  clwwlknon  27875  clwwlk0on0  27877  rmfsupp2  30917  idlsrgval  31056  rspectopn  31220  zar0ring  31231  ordtprsval  31271  snmlfval  32690  mpstval  32895  pclfvalN  37185  docaffvalN  38417  docafvalN  38418  etransclem11  42887  issmflem  43361  issmfd  43369  cnfsmf  43374  issmflelem  43378  issmfgtlem  43389  issmfgt  43390  issmfled  43391  issmfgtd  43394  issmfgelem  43402  fvmptrabdm  43849  prprspr2  44035  assintopmap  44466  dmatALTval  44809  rrxsphere  45162