Theorem csbeq1 3856

Description: Analogue of dfsbcq 3746 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbeq1	⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Proof of Theorem csbeq1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq 3746	. . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶))
2	1	abbidv 2795	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶})
3		df-csb 3854	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
4		df-csb 3854	. 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  [wsbc 3744  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745  df-csb 3854

This theorem is referenced by:  csbeq1d  3857  csbeq1a  3867  csbconstg  3872  csbiebg  3885  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbcnestgfw  4374  sbcnestgf  4379  csbun  4394  csbin  4395  csbdif  4477  csbif  4536  disjors  5078  disjxiun  5092  sbcbr123  5149  csbopab  5502  csbopabgALT  5503  pofun  5549  csbima12  6034  csbcog  6249  csbiota  6479  fvmpt2f  6935  fvmpts  6937  fvmpt2i  6944  fvmptex  6948  elfvmptrab1w  6961  elfvmptrab1  6962  fmptcof  7068  fmptcos  7069  fliftfuns  7255  csbriota  7325  riotaeqimp  7336  csbov123  7397  elovmporab1w  7600  elovmporab1  7601  el2mpocsbcl  8025  mposn  8043  mpocurryvald  8210  fvmpocurryd  8211  eqerlem  8667  qliftfuns  8738  boxcutc  8875  iunfi  9252  wdom2d  9491  summolem2a  15640  zsum  15643  fsum  15645  sumsnf  15668  sumsns  15675  fsum2dlem  15695  fsumcom2  15699  fsumshftm  15706  fsum0diag2  15708  fsumrlim  15736  fsumo1  15737  fsumiun  15746  prodmolem2a  15859  prodsn  15887  prodsnf  15889  fprodm1s  15895  fprodp1s  15896  prodsns  15897  fprod2dlem  15905  fprodcom2  15909  pcmptdvds  16824  gsummpt1n0  19862  telgsumfzslem  19885  telgsumfzs  19886  psrass1lem  21857  coe1fzgsumdlem  22206  gsummoncoe1  22211  evl1gsumdlem  22259  madugsum  22546  fiuncmp  23307  elmptrab  23730  ovolfiniun  25418  finiunmbl  25461  volfiniun  25464  iundisj  25465  iundisj2  25466  iunmbl  25470  itgfsum  25744  dvfsumle  25942  dvfsumleOLD  25943  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsum2  25957  itgsubstlem  25971  itgsubst  25972  rlimcnp2  26892  fsumdvdscom  27111  fsumdvdsmul  27121  fsumdvdsmulOLD  27123  fsumvma  27140  dchrisumlem2  27417  ifeqeqx  32504  disji2f  32539  disjorsf  32542  disjif2  32543  disjabrex  32544  disjabrexf  32545  disjxpin  32550  iundisjf  32551  iundisj2f  32552  disjunsn  32556  aciunf1lem  32619  funcnv4mpt  32626  iundisjfi  32752  iundisj2fi  32753  fsumiunle  32787  gsummpt2co  33014  itgeq12i  36179  weiunfrlem  36437  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  finixpnum  37584  poimirlem24  37623  poimirlem26  37625  csbeq12  38137  fsumshftd  38930  cdlemk54  40937  evl1gprodd  42090  idomnnzgmulnz  42106  deg1gprod  42113  mzpsubst  42721  rabdiophlem2  42775  elnn0rabdioph  42776  dvdsrabdioph  42783  fphpd  42789  monotuz  42914  oddcomabszz  42917  fnwe2lem3  43025  flcidc  43143  sumsnd  45004  disjf1  45161  disjrnmpt2  45166  climinf2mpt  45696  climinfmpt  45697  dvnmptdivc  45920  dvmptfprod  45927  fourierdlem103  46191  fourierdlem104  46192  csbafv12g  47122  csbaovg  47165  csbafv212g  47204  fargshiftfva  47428