Theorem rabeqdv 3459

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

Syntax hints:   → wi 4   = wceq 1537  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  rabeqbidvaOLD  3461  rabsnif  4748  fvmptrabfv  7061  suppvalfng  8208  suppvalfn  8209  suppsnop  8219  fnsuppres  8232  pmvalg  8895  cantnffval  9732  hashbc  14502  elovmpowrd  14606  dfphi2  16821  mrisval  17688  coafval  18131  pmtrfval  19492  dprdval  20047  rrgval  20719  lspfval  20994  lsppropd  21040  dsmmbas2  21780  frlmbas  21798  aspval  21916  mvrfval  22024  mhpfval  22165  psdffval  22184  clsfval  23054  ordtrest  23231  ordtrest2lem  23232  ordtrest2  23233  xkoval  23616  xkopt  23684  tsmsval2  24159  cncfval  24933  isphtpy  25032  cfilfval  25317  iscmet  25337  leftval  27920  rightval  27921  ttgval  28901  ttgvalOLD  28902  eengv  29012  isupgr  29119  upgrop  29129  isumgr  29130  upgrun  29153  umgrun  29155  isuspgr  29187  isusgr  29188  isuspgrop  29196  isusgrop  29197  isausgr  29199  ausgrusgrb  29200  usgrstrrepe  29270  lfuhgr1v0e  29289  usgrexi  29476  cusgrsize  29490  1loopgrvd2  29539  wwlksn  29870  wspthsn  29881  iswwlksnon  29886  iswspthsnon  29889  clwwlknonmpo  30121  clwwlknon  30122  clwwlk0on0  30124  rmfsupp2  33218  idlsrgval  33496  rspectopn  33813  zar0ring  33824  ordtprsval  33864  snmlfval  35298  mpstval  35503  pclfvalN  39846  docaffvalN  41078  docafvalN  41079  isprimroot  42050  etransclem11  46166  issmflem  46648  issmfd  46656  cnfsmf  46661  issmflelem  46665  issmfgtlem  46676  issmfgt  46677  issmfled  46678  issmfgtd  46682  issmfgelem  46690  fvmptrabdm  47208  prprspr2  47392  assintopmap  47929  mndpsuppss  48096  dmatALTval  48129  rrxsphere  48482