Theorem csbeq1 3867

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2708  [wsbc 3755  ⦋csb 3864

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3756  df-csb 3865

This theorem is referenced by:  csbeq1d  3868  csbeq1a  3878  csbconstg  3883  csbiebg  3896  cbvrabcsfw  3905  cbvralcsf  3906  cbvreucsf  3908  cbvrabcsf  3909  sbcnestgfw  4386  sbcnestgf  4391  csbun  4406  csbin  4407  csbdif  4489  csbif  4548  disjors  5092  disjxiun  5106  sbcbr123  5163  csbopab  5517  csbopabgALT  5518  pofun  5566  csbima12  6052  csbcog  6272  csbiota  6506  fvmpt2f  6971  fvmpts  6973  fvmpt2i  6980  fvmptex  6984  elfvmptrab1w  6997  elfvmptrab1  6998  fmptcof  7104  fmptcos  7105  fliftfuns  7291  csbriota  7361  riotaeqimp  7372  csbov123  7433  elovmporab1w  7638  elovmporab1  7639  el2mpocsbcl  8066  mposn  8084  mpocurryvald  8251  fvmpocurryd  8252  eqerlem  8708  qliftfuns  8779  boxcutc  8916  iunfi  9300  wdom2d  9539  summolem2a  15687  zsum  15690  fsum  15692  sumsnf  15715  sumsns  15722  fsum2dlem  15742  fsumcom2  15746  fsumshftm  15753  fsum0diag2  15755  fsumrlim  15783  fsumo1  15784  fsumiun  15793  prodmolem2a  15906  prodsn  15934  prodsnf  15936  fprodm1s  15942  fprodp1s  15943  prodsns  15944  fprod2dlem  15952  fprodcom2  15956  pcmptdvds  16871  gsummpt1n0  19901  telgsumfzslem  19924  telgsumfzs  19925  psrass1lem  21847  coe1fzgsumdlem  22196  gsummoncoe1  22201  evl1gsumdlem  22249  madugsum  22536  fiuncmp  23297  elmptrab  23720  ovolfiniun  25408  finiunmbl  25451  volfiniun  25454  iundisj  25455  iundisj2  25456  iunmbl  25460  itgfsum  25734  dvfsumle  25932  dvfsumleOLD  25933  dvfsumabs  25935  dvfsumlem2  25939  dvfsumlem2OLD  25940  dvfsumlem3  25941  dvfsumlem4  25942  dvfsum2  25947  itgsubstlem  25961  itgsubst  25962  rlimcnp2  26882  fsumdvdscom  27101  fsumdvdsmul  27111  fsumdvdsmulOLD  27113  fsumvma  27130  dchrisumlem2  27407  ifeqeqx  32477  disji2f  32512  disjorsf  32515  disjif2  32516  disjabrex  32517  disjabrexf  32518  disjxpin  32523  iundisjf  32524  iundisj2f  32525  disjunsn  32529  aciunf1lem  32592  funcnv4mpt  32599  iundisjfi  32725  iundisj2fi  32726  fsumiunle  32760  gsummpt2co  32994  itgeq12i  36189  weiunfrlem  36447  weiunpo  36448  weiunso  36449  weiunfr  36450  weiunse  36451  finixpnum  37594  poimirlem24  37633  poimirlem26  37635  csbeq12  38147  fsumshftd  38940  cdlemk54  40947  evl1gprodd  42100  idomnnzgmulnz  42116  deg1gprod  42123  mzpsubst  42729  rabdiophlem2  42783  elnn0rabdioph  42784  dvdsrabdioph  42791  fphpd  42797  monotuz  42923  oddcomabszz  42926  fnwe2lem3  43034  flcidc  43152  sumsnd  45013  disjf1  45170  disjrnmpt2  45175  climinf2mpt  45705  climinfmpt  45706  dvnmptdivc  45929  dvmptfprod  45936  fourierdlem103  46200  fourierdlem104  46201  csbafv12g  47128  csbaovg  47171  csbafv212g  47210  fargshiftfva  47434