Theorem rabeqdv 3424

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409

This theorem is referenced by:  rabeqbidvaOLD  3426  rabsnif  4690  fvmptrabfv  7003  suppvalfng  8149  suppvalfn  8150  suppsnop  8160  fnsuppres  8173  pmvalg  8813  cantnffval  9623  hashbc  14425  elovmpowrd  14530  dfphi2  16751  mrisval  17598  coafval  18033  mndpsuppss  18699  pmtrfval  19387  dprdval  19942  rrgval  20613  lspfval  20886  lsppropd  20932  dsmmbas2  21653  frlmbas  21671  aspval  21789  mvrfval  21897  mhpfval  22032  psdffval  22051  clsfval  22919  ordtrest  23096  ordtrest2lem  23097  ordtrest2  23098  xkoval  23481  xkopt  23549  tsmsval2  24024  cncfval  24788  isphtpy  24887  cfilfval  25171  iscmet  25191  leftval  27778  rightval  27779  ttgval  28809  eengv  28913  isupgr  29018  upgrop  29028  isumgr  29029  upgrun  29052  umgrun  29054  isuspgr  29086  isusgr  29087  isuspgrop  29095  isusgrop  29096  isausgr  29098  ausgrusgrb  29099  usgrstrrepe  29169  lfuhgr1v0e  29188  usgrexi  29375  cusgrsize  29389  1loopgrvd2  29438  wwlksn  29774  wspthsn  29785  iswwlksnon  29790  iswspthsnon  29793  clwwlknonmpo  30025  clwwlknon  30026  clwwlk0on0  30028  fxpgaval  33131  rmfsupp2  33196  idlsrgval  33481  rspectopn  33864  zar0ring  33875  ordtprsval  33915  snmlfval  35324  mpstval  35529  pclfvalN  39890  docaffvalN  41122  docafvalN  41123  isprimroot  42088  dvnprodlem1  45951  etransclem11  46250  issmflem  46732  issmfd  46740  cnfsmf  46745  issmflelem  46749  issmfgtlem  46760  issmfgt  46761  issmfled  46762  issmfgtd  46766  issmfgelem  46774  fvmptrabdm  47298  prprspr2  47523  stgrusgra  47962  gpgusgra  48052  assintopmap  48198  dmatALTval  48393  rrxsphere  48741  initopropdlem  49233  termopropdlem  49234