Theorem rabeqdv 3443

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

Syntax hints:   → wi 4   = wceq 1534  {crab 3428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429

This theorem is referenced by:  rabeqbidva  3444  rabsnif  4724  fvmptrabfv  7032  suppvalfng  8167  suppvalfn  8168  suppsnop  8177  fnsuppres  8190  pmvalg  8850  cantnffval  9681  hashbc  14439  elovmpowrd  14535  dfphi2  16737  mrisval  17604  coafval  18047  pmtrfval  19399  dprdval  19954  lspfval  20851  lsppropd  20897  rrgval  21228  dsmmbas2  21665  frlmbas  21683  aspval  21800  mvrfval  21917  mhpfval  22057  psdffval  22075  clsfval  22923  ordtrest  23100  ordtrest2lem  23101  ordtrest2  23102  xkoval  23485  xkopt  23553  tsmsval2  24028  cncfval  24802  isphtpy  24901  cfilfval  25186  iscmet  25206  leftval  27784  rightval  27785  ttgval  28673  ttgvalOLD  28674  eengv  28784  isupgr  28891  upgrop  28901  isumgr  28902  upgrun  28925  umgrun  28927  isuspgr  28959  isusgr  28960  isuspgrop  28968  isusgrop  28969  isausgr  28971  ausgrusgrb  28972  usgrstrrepe  29042  lfuhgr1v0e  29061  usgrexmpl  29070  usgrexi  29248  cusgrsize  29262  1loopgrvd2  29311  wwlksn  29642  wspthsn  29653  iswwlksnon  29658  iswspthsnon  29661  clwwlknonmpo  29893  clwwlknon  29894  clwwlk0on0  29896  rmfsupp2  32941  idlsrgval  33209  rspectopn  33463  zar0ring  33474  ordtprsval  33514  snmlfval  34935  mpstval  35140  pclfvalN  39357  docaffvalN  40589  docafvalN  40590  isprimroot  41559  etransclem11  45624  issmflem  46106  issmfd  46114  cnfsmf  46119  issmflelem  46123  issmfgtlem  46134  issmfgt  46135  issmfled  46136  issmfgtd  46140  issmfgelem  46148  fvmptrabdm  46664  prprspr2  46849  assintopmap  47259  mndpsuppss  47426  dmatALTval  47459  rrxsphere  47812