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  4727  fvmptrabfv  7029  suppvalfng  8155  suppvalfn  8156  suppsnop  8165  fnsuppres  8178  pmvalg  8833  cantnffval  9660  hashbc  14416  elovmpowrd  14512  dfphi2  16711  mrisval  17578  coafval  18018  pmtrfval  19359  dprdval  19914  lspfval  20728  lsppropd  20773  rrgval  21103  dsmmbas2  21511  frlmbas  21529  aspval  21646  mvrfval  21759  mhpfval  21901  clsfval  22749  ordtrest  22926  ordtrest2lem  22927  ordtrest2  22928  xkoval  23311  xkopt  23379  tsmsval2  23854  cncfval  24628  isphtpy  24721  cfilfval  25005  iscmet  25025  leftval  27583  rightval  27584  ttgval  28381  ttgvalOLD  28382  eengv  28492  isupgr  28599  upgrop  28609  isumgr  28610  upgrun  28633  umgrun  28635  isuspgr  28667  isusgr  28668  isuspgrop  28676  isusgrop  28677  isausgr  28679  ausgrusgrb  28680  usgrstrrepe  28747  lfuhgr1v0e  28766  usgrexmpl  28775  usgrexi  28953  cusgrsize  28966  1loopgrvd2  29015  wwlksn  29346  wspthsn  29357  iswwlksnon  29362  iswspthsnon  29365  clwwlknonmpo  29597  clwwlknon  29598  clwwlk0on0  29600  rmfsupp2  32645  idlsrgval  32879  rspectopn  33133  zar0ring  33144  ordtprsval  33184  snmlfval  34607  mpstval  34812  pclfvalN  39063  docaffvalN  40295  docafvalN  40296  etransclem11  45260  issmflem  45742  issmfd  45750  cnfsmf  45755  issmflelem  45759  issmfgtlem  45770  issmfgt  45771  issmfled  45772  issmfgtd  45776  issmfgelem  45784  fvmptrabdm  46300  prprspr2  46485  assintopmap  46883  mndpsuppss  47136  dmatALTval  47169  rrxsphere  47522