Theorem rabeqdv 3405

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

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

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 3391

This theorem is referenced by:  rabeqbidvaOLD  3407  rabsnif  4668  fvmptrabfv  6976  suppvalfng  8112  suppvalfn  8113  suppsnop  8123  fnsuppres  8136  pmvalg  8779  cantnffval  9579  hashbc  14410  elovmpowrd  14515  dfphi2  16739  mrisval  17591  coafval  18026  mndpsuppss  18728  pmtrfval  19420  dprdval  19975  rrgval  20669  lspfval  20963  lsppropd  21009  dsmmbas2  21731  frlmbas  21749  aspval  21866  mvrfval  21973  mhpfval  22118  psdffval  22137  clsfval  23004  ordtrest  23181  ordtrest2lem  23182  ordtrest2  23183  xkoval  23566  xkopt  23634  tsmsval2  24109  cncfval  24869  isphtpy  24962  cfilfval  25245  iscmet  25265  leftval  27859  rightval  27860  ttgval  28961  eengv  29066  isupgr  29171  upgrop  29181  isumgr  29182  upgrun  29205  umgrun  29207  isuspgr  29239  isusgr  29240  isuspgrop  29248  isusgrop  29249  isausgr  29251  ausgrusgrb  29252  usgrstrrepe  29322  lfuhgr1v0e  29341  usgrexi  29528  cusgrsize  29542  1loopgrvd2  29591  wwlksn  29924  wspthsn  29935  iswwlksnon  29940  iswspthsnon  29943  clwwlknonmpo  30178  clwwlknon  30179  clwwlk0on0  30181  fxpgaval  33247  rmfsupp2  33318  idlsrgval  33582  extvval  33694  splyval  33722  esplyval  33725  rspectopn  34031  zar0ring  34042  ordtprsval  34082  snmlfval  35532  mpstval  35737  pclfvalN  40355  docaffvalN  41587  docafvalN  41588  isprimroot  42552  dvnprodlem1  46398  etransclem11  46697  issmflem  47179  issmfd  47187  cnfsmf  47192  issmflelem  47196  issmfgtlem  47207  issmfgt  47208  issmfled  47209  issmfgtd  47213  issmfgelem  47221  fvmptrabdm  47759  prprspr2  47996  stgrusgra  48453  gpgusgra  48551  assintopmap  48700  dmatALTval  48894  rrxsphere  49242  initopropdlem  49733  termopropdlem  49734