Theorem rabeqdv 3413

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rab 3399

This theorem is referenced by:  rabeqbidvaOLD  3415  rabsnif  4679  fvmptrabfv  6973  suppvalfng  8109  suppvalfn  8110  suppsnop  8120  fnsuppres  8133  pmvalg  8776  cantnffval  9574  hashbc  14378  elovmpowrd  14483  dfphi2  16703  mrisval  17555  coafval  17990  mndpsuppss  18692  pmtrfval  19381  dprdval  19936  rrgval  20632  lspfval  20926  lsppropd  20972  dsmmbas2  21694  frlmbas  21712  aspval  21830  mvrfval  21938  mhpfval  22083  psdffval  22102  clsfval  22971  ordtrest  23148  ordtrest2lem  23149  ordtrest2  23150  xkoval  23533  xkopt  23601  tsmsval2  24076  cncfval  24839  isphtpy  24938  cfilfval  25222  iscmet  25242  leftval  27839  rightval  27840  ttgval  28928  eengv  29033  isupgr  29138  upgrop  29148  isumgr  29149  upgrun  29172  umgrun  29174  isuspgr  29206  isusgr  29207  isuspgrop  29215  isusgrop  29216  isausgr  29218  ausgrusgrb  29219  usgrstrrepe  29289  lfuhgr1v0e  29308  usgrexi  29495  cusgrsize  29509  1loopgrvd2  29558  wwlksn  29891  wspthsn  29902  iswwlksnon  29907  iswspthsnon  29910  clwwlknonmpo  30145  clwwlknon  30146  clwwlk0on0  30148  fxpgaval  33228  rmfsupp2  33299  idlsrgval  33563  extvval  33675  splyval  33696  esplyval  33699  rspectopn  34003  zar0ring  34014  ordtprsval  34054  snmlfval  35503  mpstval  35708  pclfvalN  40184  docaffvalN  41416  docafvalN  41417  isprimroot  42382  dvnprodlem1  46227  etransclem11  46526  issmflem  47008  issmfd  47016  cnfsmf  47021  issmflelem  47025  issmfgtlem  47036  issmfgt  47037  issmfled  47038  issmfgtd  47042  issmfgelem  47050  fvmptrabdm  47576  prprspr2  47801  stgrusgra  48242  gpgusgra  48340  assintopmap  48489  dmatALTval  48683  rrxsphere  49031  initopropdlem  49522  termopropdlem  49523