Theorem csbeq1 3897

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {cab 2710  [wsbc 3778  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbeq1d  3898  csbeq1a  3908  csbconstg  3913  csbiebg  3927  cbvrabcsfw  3938  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  sbcnestgfw  4419  sbcnestgf  4424  csbun  4439  csbin  4440  csbdif  4528  csbif  4586  disjors  5130  disjxiun  5146  sbcbr123  5203  csbopab  5556  csbopabgALT  5557  pofun  5607  csbima12  6079  csbcog  6297  csbiota  6537  fvmpt2f  7000  fvmpts  7002  fvmpt2i  7009  fvmptex  7013  elfvmptrab1w  7025  elfvmptrab1  7026  fmptcof  7128  fmptcos  7129  fliftfuns  7311  csbriota  7381  riotaeqimp  7392  csbov123  7451  elovmporab1w  7653  elovmporab1  7654  el2mpocsbcl  8071  mposn  8089  mpocurryvald  8255  fvmpocurryd  8256  eqerlem  8737  qliftfuns  8798  boxcutc  8935  iunfi  9340  wdom2d  9575  summolem2a  15661  zsum  15664  fsum  15666  sumsnf  15689  sumsns  15696  fsum2dlem  15716  fsumcom2  15720  fsumshftm  15727  fsum0diag2  15729  fsumrlim  15757  fsumo1  15758  fsumiun  15767  prodmolem2a  15878  prodsn  15906  prodsnf  15908  fprodm1s  15914  fprodp1s  15915  prodsns  15916  fprod2dlem  15924  fprodcom2  15928  pcmptdvds  16827  gsummpt1n0  19833  telgsumfzslem  19856  telgsumfzs  19857  psrass1lemOLD  21493  psrass1lem  21496  coe1fzgsumdlem  21825  gsummoncoe1  21828  evl1gsumdlem  21875  madugsum  22145  fiuncmp  22908  elmptrab  23331  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  iundisj  25065  iundisj2  25066  iunmbl  25070  itgfsum  25344  dvfsumle  25538  dvfsumabs  25540  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsum2  25551  itgsubstlem  25565  itgsubst  25566  rlimcnp2  26471  fsumdvdscom  26689  fsumdvdsmul  26699  fsumvma  26716  dchrisumlem2  26993  ifeqeqx  31774  disji2f  31808  disjorsf  31811  disjif2  31812  disjabrex  31813  disjabrexf  31814  disjxpin  31819  iundisjf  31820  iundisj2f  31821  disjunsn  31825  aciunf1lem  31887  funcnv4mpt  31894  iundisjfi  32007  iundisj2fi  32008  fsumiunle  32035  gsummpt2co  32200  gg-dvfsumle  35182  gg-dvfsumlem2  35183  finixpnum  36473  poimirlem24  36512  poimirlem26  36514  csbeq12  37026  fsumshftd  37822  cdlemk54  39829  mzpsubst  41486  rabdiophlem2  41540  elnn0rabdioph  41541  dvdsrabdioph  41548  fphpd  41554  monotuz  41680  oddcomabszz  41683  fnwe2lem3  41794  flcidc  41916  sumsnd  43710  disjf1  43880  disjrnmpt2  43886  climinf2mpt  44430  climinfmpt  44431  dvnmptdivc  44654  fourierdlem103  44925  fourierdlem104  44926  csbafv12g  45845  csbaovg  45888  csbafv212g  45927  fargshiftfva  46111