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  31805  disji2f  31839  disjorsf  31842  disjif2  31843  disjabrex  31844  disjabrexf  31845  disjxpin  31850  iundisjf  31851  iundisj2f  31852  disjunsn  31856  aciunf1lem  31918  funcnv4mpt  31925  iundisjfi  32038  iundisj2fi  32039  fsumiunle  32066  gsummpt2co  32231  gg-dvfsumle  35213  gg-dvfsumlem2  35214  finixpnum  36521  poimirlem24  36560  poimirlem26  36562  csbeq12  37074  fsumshftd  37870  cdlemk54  39877  mzpsubst  41534  rabdiophlem2  41588  elnn0rabdioph  41589  dvdsrabdioph  41596  fphpd  41602  monotuz  41728  oddcomabszz  41731  fnwe2lem3  41842  flcidc  41964  sumsnd  43758  disjf1  43928  disjrnmpt2  43934  climinf2mpt  44478  climinfmpt  44479  dvnmptdivc  44702  fourierdlem103  44973  fourierdlem104  44974  csbafv12g  45893  csbaovg  45936  csbafv212g  45975  fargshiftfva  46159