Theorem csbeq1 3877

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2713  [wsbc 3765  ⦋csb 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766  df-csb 3875

This theorem is referenced by:  csbeq1d  3878  csbeq1a  3888  csbconstg  3893  csbiebg  3906  cbvrabcsfw  3915  cbvralcsf  3916  cbvreucsf  3918  cbvrabcsf  3919  sbcnestgfw  4396  sbcnestgf  4401  csbun  4416  csbin  4417  csbdif  4499  csbif  4558  disjors  5102  disjxiun  5116  sbcbr123  5173  csbopab  5530  csbopabgALT  5531  pofun  5579  csbima12  6066  csbcog  6286  csbiota  6523  fvmpt2f  6986  fvmpts  6988  fvmpt2i  6995  fvmptex  6999  elfvmptrab1w  7012  elfvmptrab1  7013  fmptcof  7119  fmptcos  7120  fliftfuns  7306  csbriota  7375  riotaeqimp  7386  csbov123  7447  elovmporab1w  7652  elovmporab1  7653  el2mpocsbcl  8082  mposn  8100  mpocurryvald  8267  fvmpocurryd  8268  eqerlem  8752  qliftfuns  8816  boxcutc  8953  iunfi  9353  wdom2d  9592  summolem2a  15729  zsum  15732  fsum  15734  sumsnf  15757  sumsns  15764  fsum2dlem  15784  fsumcom2  15788  fsumshftm  15795  fsum0diag2  15797  fsumrlim  15825  fsumo1  15826  fsumiun  15835  prodmolem2a  15948  prodsn  15976  prodsnf  15978  fprodm1s  15984  fprodp1s  15985  prodsns  15986  fprod2dlem  15994  fprodcom2  15998  pcmptdvds  16912  gsummpt1n0  19944  telgsumfzslem  19967  telgsumfzs  19968  psrass1lem  21890  coe1fzgsumdlem  22239  gsummoncoe1  22244  evl1gsumdlem  22292  madugsum  22579  fiuncmp  23340  elmptrab  23763  ovolfiniun  25452  finiunmbl  25495  volfiniun  25498  iundisj  25499  iundisj2  25500  iunmbl  25504  itgfsum  25778  dvfsumle  25976  dvfsumleOLD  25977  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  itgsubstlem  26005  itgsubst  26006  rlimcnp2  26926  fsumdvdscom  27145  fsumdvdsmul  27155  fsumdvdsmulOLD  27157  fsumvma  27174  dchrisumlem2  27451  ifeqeqx  32469  disji2f  32504  disjorsf  32507  disjif2  32508  disjabrex  32509  disjabrexf  32510  disjxpin  32515  iundisjf  32516  iundisj2f  32517  disjunsn  32521  aciunf1lem  32586  funcnv4mpt  32593  iundisjfi  32719  iundisj2fi  32720  fsumiunle  32754  gsummpt2co  32988  itgeq12i  36170  weiunfrlem  36428  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  finixpnum  37575  poimirlem24  37614  poimirlem26  37616  csbeq12  38128  fsumshftd  38916  cdlemk54  40923  evl1gprodd  42076  idomnnzgmulnz  42092  deg1gprod  42099  mzpsubst  42718  rabdiophlem2  42772  elnn0rabdioph  42773  dvdsrabdioph  42780  fphpd  42786  monotuz  42912  oddcomabszz  42915  fnwe2lem3  43023  flcidc  43141  sumsnd  44998  disjf1  45155  disjrnmpt2  45160  climinf2mpt  45691  climinfmpt  45692  dvnmptdivc  45915  dvmptfprod  45922  fourierdlem103  46186  fourierdlem104  46187  csbafv12g  47114  csbaovg  47157  csbafv212g  47196  fargshiftfva  47405