Theorem csbeq1 3848

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {cab 2709  [wsbc 3736  ⦋csb 3845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sbc 3737  df-csb 3846

This theorem is referenced by:  csbeq1d  3849  csbeq1a  3859  csbconstg  3864  csbiebg  3877  cbvrabcsfw  3886  cbvralcsf  3887  cbvreucsf  3889  cbvrabcsf  3890  sbcnestgfw  4370  sbcnestgf  4375  csbun  4390  csbin  4391  csbdif  4473  csbif  4532  disjors  5076  disjxiun  5090  sbcbr123  5147  csbopab  5498  csbopabgALT  5499  pofun  5545  csbima12  6033  csbcog  6250  csbiota  6480  fvmpt2f  6936  fvmpts  6938  fvmpt2i  6945  fvmptex  6949  elfvmptrab1w  6962  elfvmptrab1  6963  fmptcof  7069  fmptcos  7070  fliftfuns  7254  csbriota  7324  riotaeqimp  7335  csbov123  7396  elovmporab1w  7599  elovmporab1  7600  el2mpocsbcl  8021  mposn  8039  mpocurryvald  8206  fvmpocurryd  8207  eqerlem  8663  qliftfuns  8734  boxcutc  8871  iunfi  9233  wdom2d  9472  summolem2a  15628  zsum  15631  fsum  15633  sumsnf  15656  sumsns  15663  fsum2dlem  15683  fsumcom2  15687  fsumshftm  15694  fsum0diag2  15696  fsumrlim  15724  fsumo1  15725  fsumiun  15734  prodmolem2a  15847  prodsn  15875  prodsnf  15877  fprodm1s  15883  fprodp1s  15884  prodsns  15885  fprod2dlem  15893  fprodcom2  15897  pcmptdvds  16812  gsummpt1n0  19883  telgsumfzslem  19906  telgsumfzs  19907  psrass1lem  21875  coe1fzgsumdlem  22224  gsummoncoe1  22229  evl1gsumdlem  22277  madugsum  22564  fiuncmp  23325  elmptrab  23748  ovolfiniun  25435  finiunmbl  25478  volfiniun  25481  iundisj  25482  iundisj2  25483  iunmbl  25487  itgfsum  25761  dvfsumle  25959  dvfsumleOLD  25960  dvfsumabs  25962  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsum2  25974  itgsubstlem  25988  itgsubst  25989  rlimcnp2  26909  fsumdvdscom  27128  fsumdvdsmul  27138  fsumdvdsmulOLD  27140  fsumvma  27157  dchrisumlem2  27434  ifeqeqx  32529  disji2f  32564  disjorsf  32567  disjif2  32568  disjabrex  32569  disjabrexf  32570  disjxpin  32575  iundisjf  32576  iundisj2f  32577  disjunsn  32581  aciunf1lem  32651  funcnv4mpt  32658  iundisjfi  32785  iundisj2fi  32786  fsumiunle  32819  gsummpt2co  33035  itgeq12i  36257  weiunfrlem  36515  weiunpo  36516  weiunso  36517  weiunfr  36518  weiunse  36519  finixpnum  37651  poimirlem24  37690  poimirlem26  37692  csbeq12  38204  fsumshftd  39057  cdlemk54  41063  evl1gprodd  42216  idomnnzgmulnz  42232  deg1gprod  42239  mzpsubst  42846  rabdiophlem2  42900  elnn0rabdioph  42901  dvdsrabdioph  42908  fphpd  42914  monotuz  43039  oddcomabszz  43042  fnwe2lem3  43150  flcidc  43268  sumsnd  45128  disjf1  45285  disjrnmpt2  45290  climinf2mpt  45817  climinfmpt  45818  dvnmptdivc  46041  dvmptfprod  46048  fourierdlem103  46312  fourierdlem104  46313  csbafv12g  47242  csbaovg  47285  csbafv212g  47324  fargshiftfva  47548