Theorem csbeq1 3924

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {cab 2717  [wsbc 3804  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805  df-csb 3922

This theorem is referenced by:  csbeq1d  3925  csbeq1a  3935  csbconstg  3940  csbiebg  3954  cbvrabcsfw  3965  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  sbcnestgfw  4444  sbcnestgf  4449  csbun  4464  csbin  4465  csbdif  4547  csbif  4605  disjors  5149  disjxiun  5163  sbcbr123  5220  csbopab  5574  csbopabgALT  5575  pofun  5626  csbima12  6108  csbcog  6328  csbiota  6566  fvmpt2f  7030  fvmpts  7032  fvmpt2i  7039  fvmptex  7043  elfvmptrab1w  7056  elfvmptrab1  7057  fmptcof  7164  fmptcos  7165  fliftfuns  7350  csbriota  7420  riotaeqimp  7431  csbov123  7492  elovmporab1w  7697  elovmporab1  7698  el2mpocsbcl  8126  mposn  8144  mpocurryvald  8311  fvmpocurryd  8312  eqerlem  8798  qliftfuns  8862  boxcutc  8999  iunfi  9411  wdom2d  9649  summolem2a  15763  zsum  15766  fsum  15768  sumsnf  15791  sumsns  15798  fsum2dlem  15818  fsumcom2  15822  fsumshftm  15829  fsum0diag2  15831  fsumrlim  15859  fsumo1  15860  fsumiun  15869  prodmolem2a  15982  prodsn  16010  prodsnf  16012  fprodm1s  16018  fprodp1s  16019  prodsns  16020  fprod2dlem  16028  fprodcom2  16032  pcmptdvds  16941  gsummpt1n0  20007  telgsumfzslem  20030  telgsumfzs  20031  psrass1lem  21975  coe1fzgsumdlem  22328  gsummoncoe1  22333  evl1gsumdlem  22381  madugsum  22670  fiuncmp  23433  elmptrab  23856  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  iundisj  25602  iundisj2  25603  iunmbl  25607  itgfsum  25882  dvfsumle  26080  dvfsumleOLD  26081  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  itgsubstlem  26109  itgsubst  26110  rlimcnp2  27027  fsumdvdscom  27246  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  fsumvma  27275  dchrisumlem2  27552  ifeqeqx  32565  disji2f  32599  disjorsf  32602  disjif2  32603  disjabrex  32604  disjabrexf  32605  disjxpin  32610  iundisjf  32611  iundisj2f  32612  disjunsn  32616  aciunf1lem  32680  funcnv4mpt  32687  iundisjfi  32801  iundisj2fi  32802  fsumiunle  32833  gsummpt2co  33031  itgeq12i  36170  weiunfrlem  36430  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  finixpnum  37565  poimirlem24  37604  poimirlem26  37606  csbeq12  38118  fsumshftd  38908  cdlemk54  40915  evl1gprodd  42074  idomnnzgmulnz  42090  deg1gprod  42097  mzpsubst  42704  rabdiophlem2  42758  elnn0rabdioph  42759  dvdsrabdioph  42766  fphpd  42772  monotuz  42898  oddcomabszz  42901  fnwe2lem3  43009  flcidc  43131  sumsnd  44926  disjf1  45090  disjrnmpt2  45095  climinf2mpt  45635  climinfmpt  45636  dvnmptdivc  45859  fourierdlem103  46130  fourierdlem104  46131  csbafv12g  47052  csbaovg  47095  csbafv212g  47134  fargshiftfva  47317