Theorem csbeq1 3896

Description: Analogue of dfsbcq 3779 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 3779	. . 3 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝑦 ∈ 𝐶 ↔ [𝐵 / 𝑥]𝑦 ∈ 𝐶))
2	1	abbidv 2800	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶})
3		df-csb 3894	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
4		df-csb 3894	. 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  {cab 2708  [wsbc 3777  ⦋csb 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-sbc 3778  df-csb 3894

This theorem is referenced by:  csbeq1d  3897  csbeq1a  3907  csbconstg  3912  csbiebg  3926  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbcnestgfw  4418  sbcnestgf  4423  csbun  4438  csbin  4439  csbdif  4527  csbif  4585  disjors  5129  disjxiun  5145  sbcbr123  5202  csbopab  5555  csbopabgALT  5556  pofun  5606  csbima12  6078  csbcog  6296  csbiota  6536  fvmpt2f  6999  fvmpts  7001  fvmpt2i  7008  fvmptex  7012  elfvmptrab1w  7024  elfvmptrab1  7025  fmptcof  7130  fmptcos  7131  fliftfuns  7314  csbriota  7384  riotaeqimp  7395  csbov123  7454  elovmporab1w  7657  elovmporab1  7658  el2mpocsbcl  8076  mposn  8094  mpocurryvald  8261  fvmpocurryd  8262  eqerlem  8743  qliftfuns  8804  boxcutc  8941  iunfi  9346  wdom2d  9581  summolem2a  15668  zsum  15671  fsum  15673  sumsnf  15696  sumsns  15703  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsum0diag2  15736  fsumrlim  15764  fsumo1  15765  fsumiun  15774  prodmolem2a  15885  prodsn  15913  prodsnf  15915  fprodm1s  15921  fprodp1s  15922  prodsns  15923  fprod2dlem  15931  fprodcom2  15935  pcmptdvds  16834  gsummpt1n0  19878  telgsumfzslem  19901  telgsumfzs  19902  psrass1lemOLD  21716  psrass1lem  21719  coe1fzgsumdlem  22058  gsummoncoe1  22061  evl1gsumdlem  22108  madugsum  22378  fiuncmp  23141  elmptrab  23564  ovolfiniun  25263  finiunmbl  25306  volfiniun  25309  iundisj  25310  iundisj2  25311  iunmbl  25315  itgfsum  25589  dvfsumle  25787  dvfsumabs  25789  dvfsumlem2  25793  dvfsumlem3  25794  dvfsumlem4  25795  dvfsum2  25800  itgsubstlem  25814  itgsubst  25815  rlimcnp2  26722  fsumdvdscom  26940  fsumdvdsmul  26950  fsumvma  26967  dchrisumlem2  27244  ifeqeqx  32056  disji2f  32090  disjorsf  32093  disjif2  32094  disjabrex  32095  disjabrexf  32096  disjxpin  32101  iundisjf  32102  iundisj2f  32103  disjunsn  32107  aciunf1lem  32169  funcnv4mpt  32176  iundisjfi  32289  iundisj2fi  32290  fsumiunle  32317  gsummpt2co  32485  gg-dvfsumle  35479  gg-dvfsumlem2  35480  finixpnum  36789  poimirlem24  36828  poimirlem26  36830  csbeq12  37342  fsumshftd  38138  cdlemk54  40145  mzpsubst  41801  rabdiophlem2  41855  elnn0rabdioph  41856  dvdsrabdioph  41863  fphpd  41869  monotuz  41995  oddcomabszz  41998  fnwe2lem3  42109  flcidc  42231  sumsnd  44025  disjf1  44193  disjrnmpt2  44198  climinf2mpt  44741  climinfmpt  44742  dvnmptdivc  44965  fourierdlem103  45236  fourierdlem104  45237  csbafv12g  46156  csbaovg  46199  csbafv212g  46238  fargshiftfva  46422