Theorem rabeqdv 3410

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  rabeqbidvaOLD  3412  rabsnif  4673  fvmptrabfv  6961  suppvalfng  8097  suppvalfn  8098  suppsnop  8108  fnsuppres  8121  pmvalg  8761  cantnffval  9553  hashbc  14360  elovmpowrd  14465  dfphi2  16685  mrisval  17536  coafval  17971  mndpsuppss  18673  pmtrfval  19362  dprdval  19917  rrgval  20612  lspfval  20906  lsppropd  20952  dsmmbas2  21674  frlmbas  21692  aspval  21810  mvrfval  21918  mhpfval  22053  psdffval  22072  clsfval  22940  ordtrest  23117  ordtrest2lem  23118  ordtrest2  23119  xkoval  23502  xkopt  23570  tsmsval2  24045  cncfval  24808  isphtpy  24907  cfilfval  25191  iscmet  25211  leftval  27804  rightval  27805  ttgval  28853  eengv  28957  isupgr  29062  upgrop  29072  isumgr  29073  upgrun  29096  umgrun  29098  isuspgr  29130  isusgr  29131  isuspgrop  29139  isusgrop  29140  isausgr  29142  ausgrusgrb  29143  usgrstrrepe  29213  lfuhgr1v0e  29232  usgrexi  29419  cusgrsize  29433  1loopgrvd2  29482  wwlksn  29815  wspthsn  29826  iswwlksnon  29831  iswspthsnon  29834  clwwlknonmpo  30069  clwwlknon  30070  clwwlk0on0  30072  fxpgaval  33136  rmfsupp2  33205  idlsrgval  33468  splyval  33582  esplyval  33585  rspectopn  33880  zar0ring  33891  ordtprsval  33931  snmlfval  35374  mpstval  35579  pclfvalN  39987  docaffvalN  41219  docafvalN  41220  isprimroot  42185  dvnprodlem1  46043  etransclem11  46342  issmflem  46824  issmfd  46832  cnfsmf  46837  issmflelem  46841  issmfgtlem  46852  issmfgt  46853  issmfled  46854  issmfgtd  46858  issmfgelem  46866  fvmptrabdm  47392  prprspr2  47617  stgrusgra  48058  gpgusgra  48156  assintopmap  48305  dmatALTval  48500  rrxsphere  48848  initopropdlem  49340  termopropdlem  49341