Theorem csbeq1 3855

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  {cab 2739  [wsbc 3743  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3744  df-csb 3853

This theorem is referenced by:  csbeq1d  3856  csbeq1a  3866  csbconstg  3871  csbiebg  3884  cbvrabcsfw  3893  cbvralcsf  3894  cbvreucsf  3896  cbvrabcsf  3897  sbcnestgfw  4385  sbcnestgf  4390  csbun  4405  csbin  4406  csbdif  4485  csbif  4544  disjors  5091  disjxiun  5105  sbcbr123  5164  csbopab  5540  csbopabw  5541  pofun  5587  csbima12  6081  csbcog  6298  csbiota  6529  fvmpt2f  6990  fvmpts  6993  fvmpt2i  7000  fvmptex  7004  elfvmptrab1w  7017  elfvmptrab1  7018  fmptcof  7126  fmptcos  7127  fliftfuns  7312  csbriota  7382  riotaeqimp  7393  csbov123  7454  elovmporab1w  7657  elovmporab1  7658  el2mpocsbcl  8079  mposn  8097  mpocurryvald  8265  fvmpocurryd  8266  eqerlem  8729  qliftfuns  8801  boxcutc  8938  iunfi  9299  wdom2d  9541  summolem2a  15765  zsum  15768  fsum  15770  sumsnf  15793  sumsns  15800  fsum2dlem  15820  fsumcom2  15824  fsumshftm  15831  fsum0diag2  15833  fsumrlim  15862  fsumo1  15863  fsumiun  15872  prodmolem2a  15987  prodsn  16015  prodsnf  16017  fprodm1s  16023  fprodp1s  16024  prodsns  16025  fprod2dlem  16033  fprodcom2  16037  pcmptdvds  16953  gsummpt1n0  20034  telgsumfzslem  20057  telgsumfzs  20058  psrass1lem  22062  coe1fzgsumdlem  22442  gsummoncoe1  22447  evl1gsumdlem  22495  madugsum  22779  fiuncmp  23540  elmptrab  23963  ovolfiniun  25639  finiunmbl  25682  volfiniun  25685  iundisj  25686  iundisj2  25687  iunmbl  25691  itgfsum  25965  dvfsumle  26159  dvfsumabs  26161  dvfsumlem2  26165  dvfsumlem3  26166  dvfsumlem4  26167  dvfsum2  26172  itgsubstlem  26186  itgsubst  26187  rlimcnp2  27107  fsumdvdscom  27325  fsumdvdsmul  27335  fsumvma  27353  dchrisumlem2  27630  ifeqeqx  32854  disji2f  32888  disjorsf  32891  disjif2  32892  disjabrex  32893  disjabrexf  32894  disjxpin  32899  iundisjf  32900  iundisj2f  32901  disjunsn  32905  aciunf1lem  32973  funcnv4mpt  32979  iundisjfi  33107  iundisj2fi  33108  fsumiunle  33139  gsummpt2co  33334  itgeq12i  36662  weiunfrlem  36919  weiunpo  36920  weiunso  36921  weiunfr  36922  weiunse  36923  csbttc  36964  finixpnum  38200  poimirlem24  38239  poimirlem26  38241  csbeq12  38753  fsumshftd  39672  cdlemk54  41678  evl1gprodd  42830  idomnnzgmulnz  42846  deg1gprod  42853  mzpsubst  43427  rabdiophlem2  43477  elnn0rabdioph  43478  dvdsrabdioph  43485  fphpd  43491  monotuz  43616  oddcomabszz  43619  fnwe2lem3  43727  flcidc  43845  sumsnd  45694  disjf1  45849  disjrnmpt2  45854  climinf2mpt  46376  climinfmpt  46377  dvnmptdivc  46600  dvmptfprod  46607  fourierdlem103  46871  fourierdlem104  46872  csbafv12g  47819  csbaovg  47862  csbafv212g  47901  fargshiftfva  48137