Theorem rabeqdv 3447

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

Syntax hints:   → wi 4   = wceq 1541  {crab 3432

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433

This theorem is referenced by:  rabeqbidva  3448  rabsnif  4726  fvmptrabfv  7026  suppvalfng  8149  suppvalfn  8150  suppsnop  8159  fnsuppres  8172  pmvalg  8827  cantnffval  9654  hashbc  14408  elovmpowrd  14504  dfphi2  16703  mrisval  17570  coafval  18010  pmtrfval  19312  dprdval  19867  lspfval  20576  lsppropd  20621  rrgval  20895  dsmmbas2  21283  frlmbas  21301  aspval  21418  mvrfval  21531  mhpfval  21673  clsfval  22520  ordtrest  22697  ordtrest2lem  22698  ordtrest2  22699  xkoval  23082  xkopt  23150  tsmsval2  23625  cncfval  24395  isphtpy  24488  cfilfval  24772  iscmet  24792  leftval  27347  rightval  27348  ttgval  28115  ttgvalOLD  28116  eengv  28226  isupgr  28333  upgrop  28343  isumgr  28344  upgrun  28367  umgrun  28369  isuspgr  28401  isusgr  28402  isuspgrop  28410  isusgrop  28411  isausgr  28413  ausgrusgrb  28414  usgrstrrepe  28481  lfuhgr1v0e  28500  usgrexmpl  28509  usgrexi  28687  cusgrsize  28700  1loopgrvd2  28749  wwlksn  29080  wspthsn  29091  iswwlksnon  29096  iswspthsnon  29099  clwwlknonmpo  29331  clwwlknon  29332  clwwlk0on0  29334  rmfsupp2  32375  idlsrgval  32605  rspectopn  32835  zar0ring  32846  ordtprsval  32886  snmlfval  34309  mpstval  34514  pclfvalN  38748  docaffvalN  39980  docafvalN  39981  etransclem11  44947  issmflem  45429  issmfd  45437  cnfsmf  45442  issmflelem  45446  issmfgtlem  45457  issmfgt  45458  issmfled  45459  issmfgtd  45463  issmfgelem  45471  fvmptrabdm  45987  prprspr2  46172  assintopmap  46602  mndpsuppss  47000  dmatALTval  47034  rrxsphere  47387