Theorem rabeqdv 3415

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

Syntax hints:   → wi 4   = wceq 1542  {crab 3400

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401

This theorem is referenced by:  rabeqbidvaOLD  3417  rabsnif  4681  fvmptrabfv  6975  suppvalfng  8111  suppvalfn  8112  suppsnop  8122  fnsuppres  8135  pmvalg  8778  cantnffval  9576  hashbc  14380  elovmpowrd  14485  dfphi2  16705  mrisval  17557  coafval  17992  mndpsuppss  18694  pmtrfval  19383  dprdval  19938  rrgval  20634  lspfval  20928  lsppropd  20974  dsmmbas2  21696  frlmbas  21714  aspval  21832  mvrfval  21940  mhpfval  22085  psdffval  22104  clsfval  22973  ordtrest  23150  ordtrest2lem  23151  ordtrest2  23152  xkoval  23535  xkopt  23603  tsmsval2  24078  cncfval  24841  isphtpy  24940  cfilfval  25224  iscmet  25244  leftval  27849  rightval  27850  ttgval  28951  eengv  29056  isupgr  29161  upgrop  29171  isumgr  29172  upgrun  29195  umgrun  29197  isuspgr  29229  isusgr  29230  isuspgrop  29238  isusgrop  29239  isausgr  29241  ausgrusgrb  29242  usgrstrrepe  29312  lfuhgr1v0e  29331  usgrexi  29518  cusgrsize  29532  1loopgrvd2  29581  wwlksn  29914  wspthsn  29925  iswwlksnon  29930  iswspthsnon  29933  clwwlknonmpo  30168  clwwlknon  30169  clwwlk0on0  30171  fxpgaval  33251  rmfsupp2  33322  idlsrgval  33586  extvval  33698  splyval  33719  esplyval  33722  rspectopn  34026  zar0ring  34037  ordtprsval  34077  snmlfval  35526  mpstval  35731  pclfvalN  40217  docaffvalN  41449  docafvalN  41450  isprimroot  42415  dvnprodlem1  46257  etransclem11  46556  issmflem  47038  issmfd  47046  cnfsmf  47051  issmflelem  47055  issmfgtlem  47066  issmfgt  47067  issmfled  47068  issmfgtd  47072  issmfgelem  47080  fvmptrabdm  47606  prprspr2  47831  stgrusgra  48272  gpgusgra  48370  assintopmap  48519  dmatALTval  48713  rrxsphere  49061  initopropdlem  49552  termopropdlem  49553