Theorem csbeq1 3849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2738  [wsbc 3738  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sbc 3739  df-csb 3847

This theorem is used by:  csbeq1d  3850  csbeq1a  3860  csbconstg  3865  csbiebg  3878  cbvrabcsfw  3887  cbvralcsf  3888  cbvreucsf  3890  cbvrabcsf  3891  sbcnestgfw  4378  sbcnestgf  4383  csbun  4398  csbin  4399  csbdif  4480  csbif  4539  disjors  5085  disjxiun  5099  sbcbr123  5158  csbopab  5526  csbopabw  5527  pofun  5573  csbima12  6069  csbcog  6289  csbiota  6520  fvmpt2f  6982  fvmpts  6985  fvmpt2i  6992  fvmptex  6996  elfvmptrab1w  7009  elfvmptrab1  7010  fmptcof  7119  fmptcos  7120  fliftfuns  7310  csbriota  7380  riotaeqimp  7391  csbov123  7452  elovmporab1w  7656  elovmporab1  7657  el2mpocsbcl  8079  mposn  8097  mpocurryvald  8265  fvmpocurryd  8266  eqerlem  8731  qliftfuns  8803  boxcutc  8947  iunfi  9310  wdom2d  9552  summolem2a  15848  zsum  15851  fsum  15853  sumsnf  15876  sumsns  15883  fsum2dlem  15903  fsumcom2  15907  fsumshftm  15914  fsum0diag2  15916  fsumrlim  15945  fsumo1  15946  fsumiun  15955  prodmolem2a  16068  prodsn  16096  prodsnf  16098  fprodm1s  16104  fprodp1s  16105  prodsns  16106  fprod2dlem  16114  fprodcom2  16118  pcmptdvds  17033  gsummpt1n0  20140  telgsumfzslem  20163  telgsumfzs  20164  psrass1lem  22202  coe1fzgsumdlem  22582  gsummoncoe1  22587  evl1gsumdlem  22635  madugsum  22919  fiuncmp  23683  elmptrab  24107  ovolfiniun  25783  finiunmbl  25826  volfiniun  25829  iundisj  25830  iundisj2  25831  iunmbl  25835  itgfsum  26108  dvfsumle  26302  dvfsumabs  26304  dvfsumlem2  26308  dvfsumlem3  26309  dvfsumlem4  26310  dvfsum2  26315  itgsubstlem  26329  itgsubst  26330  rlimcnp2  27257  fsumdvdscom  27475  fsumdvdsmul  27485  fsumvma  27503  dchrisumlem2  27780  ifeqeqx  33071  disji2f  33104  disjorsf  33107  disjif2  33108  disjabrex  33109  disjabrexf  33110  disjxpin  33115  iundisjf  33116  iundisj2f  33117  disjunsn  33121  aciunf1lem  33189  funcnv4mpt  33195  iundisjfi  33321  iundisj2fi  33322  fsumiunle  33353  gsummpt2co  33542  itgeq12i  36917  weiunfrlem  37174  weiunpo  37175  weiunso  37176  weiunfr  37177  weiunse  37178  csbttc  37219  finixpnum  38448  poimirlem24  38482  poimirlem26  38484  csbeq12  39010  fsumshftd  39929  cdlemk54  41935  evl1gprodd  43087  idomnnzgmulnz  43103  deg1gprod  43110  mzpsubst  43697  rabdiophlem2  43747  elnn0rabdioph  43748  dvdsrabdioph  43755  fphpd  43761  monotuz  43886  oddcomabszz  43889  fnwe2lem3  43997  flcidc  44115  sumsnd  45964  disjf1  46119  disjrnmpt2  46124  climinf2mpt  46646  climinfmpt  46647  dvnmptdivc  46870  dvmptfprod  46877  fourierdlem103  47141  fourierdlem104  47142  csbafv12g  48129  csbaovg  48172  csbafv212g  48211  fargshiftfva  48447