Theorem rabeqdv 3421

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406

This theorem is referenced by:  rabeqbidvaOLD  3423  rabsnif  4687  fvmptrabfv  7000  suppvalfng  8146  suppvalfn  8147  suppsnop  8157  fnsuppres  8170  pmvalg  8810  cantnffval  9616  hashbc  14418  elovmpowrd  14523  dfphi2  16744  mrisval  17591  coafval  18026  mndpsuppss  18692  pmtrfval  19380  dprdval  19935  rrgval  20606  lspfval  20879  lsppropd  20925  dsmmbas2  21646  frlmbas  21664  aspval  21782  mvrfval  21890  mhpfval  22025  psdffval  22044  clsfval  22912  ordtrest  23089  ordtrest2lem  23090  ordtrest2  23091  xkoval  23474  xkopt  23542  tsmsval2  24017  cncfval  24781  isphtpy  24880  cfilfval  25164  iscmet  25184  leftval  27771  rightval  27772  ttgval  28802  eengv  28906  isupgr  29011  upgrop  29021  isumgr  29022  upgrun  29045  umgrun  29047  isuspgr  29079  isusgr  29080  isuspgrop  29088  isusgrop  29089  isausgr  29091  ausgrusgrb  29092  usgrstrrepe  29162  lfuhgr1v0e  29181  usgrexi  29368  cusgrsize  29382  1loopgrvd2  29431  wwlksn  29767  wspthsn  29778  iswwlksnon  29783  iswspthsnon  29786  clwwlknonmpo  30018  clwwlknon  30019  clwwlk0on0  30021  fxpgaval  33124  rmfsupp2  33189  idlsrgval  33474  rspectopn  33857  zar0ring  33868  ordtprsval  33908  snmlfval  35317  mpstval  35522  pclfvalN  39883  docaffvalN  41115  docafvalN  41116  isprimroot  42081  dvnprodlem1  45944  etransclem11  46243  issmflem  46725  issmfd  46733  cnfsmf  46738  issmflelem  46742  issmfgtlem  46753  issmfgt  46754  issmfled  46755  issmfgtd  46759  issmfgelem  46767  fvmptrabdm  47294  prprspr2  47519  stgrusgra  47958  gpgusgra  48048  assintopmap  48194  dmatALTval  48389  rrxsphere  48737  initopropdlem  49229  termopropdlem  49230