Theorem rabeqdv 3416

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

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

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 3402

This theorem is referenced by:  rabeqbidvaOLD  3418  rabsnif  4682  fvmptrabfv  6984  suppvalfng  8121  suppvalfn  8122  suppsnop  8132  fnsuppres  8145  pmvalg  8788  cantnffval  9586  hashbc  14390  elovmpowrd  14495  dfphi2  16715  mrisval  17567  coafval  18002  mndpsuppss  18704  pmtrfval  19396  dprdval  19951  rrgval  20647  lspfval  20941  lsppropd  20987  dsmmbas2  21709  frlmbas  21727  aspval  21845  mvrfval  21953  mhpfval  22098  psdffval  22117  clsfval  22986  ordtrest  23163  ordtrest2lem  23164  ordtrest2  23165  xkoval  23548  xkopt  23616  tsmsval2  24091  cncfval  24854  isphtpy  24953  cfilfval  25237  iscmet  25257  leftval  27862  rightval  27863  ttgval  28965  eengv  29070  isupgr  29175  upgrop  29185  isumgr  29186  upgrun  29209  umgrun  29211  isuspgr  29243  isusgr  29244  isuspgrop  29252  isusgrop  29253  isausgr  29255  ausgrusgrb  29256  usgrstrrepe  29326  lfuhgr1v0e  29345  usgrexi  29532  cusgrsize  29546  1loopgrvd2  29595  wwlksn  29928  wspthsn  29939  iswwlksnon  29944  iswspthsnon  29947  clwwlknonmpo  30182  clwwlknon  30183  clwwlk0on0  30185  fxpgaval  33267  rmfsupp2  33338  idlsrgval  33602  extvval  33714  splyval  33742  esplyval  33745  rspectopn  34051  zar0ring  34062  ordtprsval  34102  snmlfval  35552  mpstval  35757  pclfvalN  40294  docaffvalN  41526  docafvalN  41527  isprimroot  42492  dvnprodlem1  46333  etransclem11  46632  issmflem  47114  issmfd  47122  cnfsmf  47127  issmflelem  47131  issmfgtlem  47142  issmfgt  47143  issmfled  47144  issmfgtd  47148  issmfgelem  47156  fvmptrabdm  47682  prprspr2  47907  stgrusgra  48348  gpgusgra  48446  assintopmap  48595  dmatALTval  48789  rrxsphere  49137  initopropdlem  49628  termopropdlem  49629