Theorem rabeqdv 3417

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074

This theorem is referenced by:  rabeqbidv  3418  rabeqbidva  3419  rabsnif  4664  fvmptrabfv  6900  suppvalfng  7968  suppvalfn  7969  suppsnop  7978  fnsuppres  7991  pmvalg  8600  cantnffval  9382  hashbc  14146  elovmpowrd  14242  dfphi2  16456  mrisval  17320  coafval  17760  pmtrfval  19039  dprdval  19587  lspfval  20216  lsppropd  20261  rrgval  20539  dsmmbas2  20925  frlmbas  20943  aspval  21058  mvrfval  21170  mhpfval  21310  clsfval  22157  ordtrest  22334  ordtrest2lem  22335  ordtrest2  22336  xkoval  22719  xkopt  22787  tsmsval2  23262  cncfval  24032  isphtpy  24125  cfilfval  24409  iscmet  24429  ttgval  27217  ttgvalOLD  27218  eengv  27328  isupgr  27435  upgrop  27445  isumgr  27446  upgrun  27469  umgrun  27471  isuspgr  27503  isusgr  27504  isuspgrop  27512  isusgrop  27513  isausgr  27515  ausgrusgrb  27516  usgrstrrepe  27583  lfuhgr1v0e  27602  usgrexmpl  27611  usgrexi  27789  cusgrsize  27802  1loopgrvd2  27851  wwlksn  28181  wspthsn  28192  iswwlksnon  28197  iswspthsnon  28200  clwwlknonmpo  28432  clwwlknon  28433  clwwlk0on0  28435  rmfsupp2  31471  idlsrgval  31627  rspectopn  31796  zar0ring  31807  ordtprsval  31847  snmlfval  33271  mpstval  33476  leftval  34026  rightval  34027  pclfvalN  37882  docaffvalN  39114  docafvalN  39115  etransclem11  43740  issmflem  44214  issmfd  44222  cnfsmf  44227  issmflelem  44231  issmfgtlem  44242  issmfgt  44243  issmfled  44244  issmfgtd  44247  issmfgelem  44255  fvmptrabdm  44736  prprspr2  44922  assintopmap  45352  mndpsuppss  45659  dmatALTval  45693  rrxsphere  46046