Theorem rabeqdv 3431

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  rabsnif  4684  fvmptrabfv  7046  suppvalfng  8209  suppvalfn  8210  suppsnop  8220  fnsuppres  8233  pmvalg  8882  cantnffval  9688  hashbc  14622  elovmpowrd  14727  dfphi2  16977  mrisval  17830  coafval  18265  mndpsuppss  18985  pmtrfval  19691  dprdval  20246  rrgval  20976  lspfval  21275  lsppropd  21320  rspvalint  21550  dsmmbas2  22070  frlmbas  22088  aspval  22207  mvrfval  22315  mhpfval  22486  psdffval  22505  clsfval  23370  ordtrest  23547  ordtrest2lem  23548  ordtrest2  23549  xkoval  23933  xkopt  24001  tsmsval2  24476  cncfval  25236  isphtpy  25329  cfilfval  25612  iscmet  25632  leftval  28262  rightval  28263  angmgmval  29421  ttgval  29479  eengv  29584  isupgr  29689  upgrop  29699  isumgr  29700  upgrun  29723  umgrun  29725  isuspgr  29760  isusgr  29761  isuspgrop  29769  isusgrop  29770  isausgr  29772  ausgrusgrb  29773  usgrstrrepe  29843  lfuhgr1v0e  29862  usgrexi  30049  cusgrsize  30062  1loopgrvd2  30111  wwlksn  30453  wspthsn  30464  iswwlksnon  30469  iswspthsnon  30472  clwwlknonmpo  30707  clwwlknon  30708  clwwlk0on0  30710  fxpgaval  33795  rmfsupp2  33865  idlsrgval  34102  extvval  34230  splyval  34258  esplyval  34261  rspectopn  34566  zar0ring  34577  ordtprsval  34617  snmlfval  36261  mpstval  36466  pclfvalN  41137  docaffvalN  42369  docafvalN  42370  isprimroot  43334  dvnprodlem1  47159  etransclem11  47458  issmflem  47940  issmfd  47948  cnfsmf  47953  issmflelem  47957  issmfgtlem  47968  issmfgt  47969  issmfled  47970  issmfgtd  47974  issmfgelem  47982  fvmptrabdm  48566  prprspr2  48803  stgrusgra  49260  gpgusgra  49358  assintopmap  49506  dmatALTval  49715  rrxsphere  50063  initopropdlem  50565  termopropdlem  50566