Theorem csbeq1 3814

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  {cab 2714  [wsbc 3694  ⦋csb 3811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-sbc 3695  df-csb 3812

This theorem is referenced by:  csbeq1d  3815  csbeq1a  3825  csbconstg  3830  csbiebg  3844  cbvrabcsfw  3855  cbvralcsf  3856  cbvreucsf  3858  cbvrabcsf  3859  sbcnestgfw  4333  sbcnestgf  4338  csbun  4353  csbin  4354  csbif  4496  disjors  5034  disjxiun  5050  sbcbr123  5107  csbopab  5436  csbopabgALT  5437  pofun  5486  csbima12  5947  csbiota  6373  fvmpt2f  6819  fvmpts  6821  fvmpt2i  6828  fvmptex  6832  elfvmptrab1w  6844  elfvmptrab1  6845  fmptcof  6945  fmptcos  6946  fliftfuns  7123  csbriota  7186  riotaeqimp  7197  csbov123  7255  elovmporab1w  7452  elovmporab1  7453  el2mpocsbcl  7853  mposn  7871  mpocurryvald  8012  fvmpocurryd  8013  eqerlem  8425  qliftfuns  8486  boxcutc  8622  iunfi  8964  wdom2d  9196  summolem2a  15279  zsum  15282  fsum  15284  sumsnf  15307  sumsns  15314  fsum2dlem  15334  fsumcom2  15338  fsumshftm  15345  fsum0diag2  15347  fsumrlim  15375  fsumo1  15376  fsumiun  15385  prodmolem2a  15496  prodsn  15524  prodsnf  15526  fprodm1s  15532  fprodp1s  15533  prodsns  15534  fprod2dlem  15542  fprodcom2  15546  pcmptdvds  16447  gsummpt1n0  19350  telgsumfzslem  19373  telgsumfzs  19374  psrass1lemOLD  20899  psrass1lem  20902  coe1fzgsumdlem  21222  gsummoncoe1  21225  evl1gsumdlem  21272  madugsum  21540  fiuncmp  22301  elmptrab  22724  ovolfiniun  24398  finiunmbl  24441  volfiniun  24444  iundisj  24445  iundisj2  24446  iunmbl  24450  itgfsum  24724  dvfsumle  24918  dvfsumabs  24920  dvfsumlem2  24924  dvfsumlem3  24925  dvfsumlem4  24926  dvfsum2  24931  itgsubstlem  24945  itgsubst  24946  rlimcnp2  25849  fsumdvdscom  26067  fsumdvdsmul  26077  fsumvma  26094  dchrisumlem2  26371  ifeqeqx  30604  disji2f  30635  disjorsf  30638  disjif2  30639  disjabrex  30640  disjabrexf  30641  disjxpin  30646  iundisjf  30647  iundisj2f  30648  disjunsn  30652  aciunf1lem  30719  funcnv4mpt  30726  iundisjfi  30837  iundisj2fi  30838  fsumiunle  30863  gsummpt2co  31027  csbdif  35233  finixpnum  35499  poimirlem24  35538  poimirlem26  35540  csbeq12  36053  fsumshftd  36703  cdlemk54  38709  mzpsubst  40273  rabdiophlem2  40327  elnn0rabdioph  40328  dvdsrabdioph  40335  fphpd  40341  monotuz  40466  oddcomabszz  40469  fnwe2lem3  40580  flcidc  40702  csbcog  40934  sumsnd  42242  disjf1  42393  disjrnmpt2  42399  climinf2mpt  42930  climinfmpt  42931  dvnmptdivc  43154  fourierdlem103  43425  fourierdlem104  43426  csbafv12g  44301  csbaovg  44344  csbafv212g  44383  fargshiftfva  44568