Theorem rabeqdv 3429

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

Syntax hints:   → wi 4   = wceq 1539  {crab 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414

This theorem is referenced by:  rabeqbidvaOLD  3431  rabsnif  4696  fvmptrabfv  7014  suppvalfng  8160  suppvalfn  8161  suppsnop  8171  fnsuppres  8184  pmvalg  8845  cantnffval  9669  hashbc  14459  elovmpowrd  14563  dfphi2  16778  mrisval  17627  coafval  18062  mndpsuppss  18728  pmtrfval  19416  dprdval  19971  rrgval  20642  lspfval  20915  lsppropd  20961  dsmmbas2  21682  frlmbas  21700  aspval  21818  mvrfval  21926  mhpfval  22061  psdffval  22080  clsfval  22948  ordtrest  23125  ordtrest2lem  23126  ordtrest2  23127  xkoval  23510  xkopt  23578  tsmsval2  24053  cncfval  24817  isphtpy  24916  cfilfval  25201  iscmet  25221  leftval  27805  rightval  27806  ttgval  28786  eengv  28890  isupgr  28995  upgrop  29005  isumgr  29006  upgrun  29029  umgrun  29031  isuspgr  29063  isusgr  29064  isuspgrop  29072  isusgrop  29073  isausgr  29075  ausgrusgrb  29076  usgrstrrepe  29146  lfuhgr1v0e  29165  usgrexi  29352  cusgrsize  29366  1loopgrvd2  29415  wwlksn  29751  wspthsn  29762  iswwlksnon  29767  iswspthsnon  29770  clwwlknonmpo  30002  clwwlknon  30003  clwwlk0on0  30005  rmfsupp2  33151  idlsrgval  33436  rspectopn  33806  zar0ring  33817  ordtprsval  33857  snmlfval  35273  mpstval  35478  pclfvalN  39829  docaffvalN  41061  docafvalN  41062  isprimroot  42028  dvnprodlem1  45905  etransclem11  46204  issmflem  46686  issmfd  46694  cnfsmf  46699  issmflelem  46703  issmfgtlem  46714  issmfgt  46715  issmfled  46716  issmfgtd  46720  issmfgelem  46728  fvmptrabdm  47250  prprspr2  47450  stgrusgra  47871  gpgusgra  47957  assintopmap  48067  dmatALTval  48262  rrxsphere  48614  initopropdlem  48963  termopropdlem  48964