Theorem csbeq1 3910

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  {cab 2711  [wsbc 3790  ⦋csb 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sbc 3791  df-csb 3908

This theorem is referenced by:  csbeq1d  3911  csbeq1a  3921  csbconstg  3926  csbiebg  3940  cbvrabcsfw  3951  cbvralcsf  3952  cbvreucsf  3954  cbvrabcsf  3955  sbcnestgfw  4426  sbcnestgf  4431  csbun  4446  csbin  4447  csbdif  4529  csbif  4587  disjors  5130  disjxiun  5144  sbcbr123  5201  csbopab  5564  csbopabgALT  5565  pofun  5614  csbima12  6098  csbcog  6318  csbiota  6555  fvmpt2f  7016  fvmpts  7018  fvmpt2i  7025  fvmptex  7029  elfvmptrab1w  7042  elfvmptrab1  7043  fmptcof  7149  fmptcos  7150  fliftfuns  7333  csbriota  7402  riotaeqimp  7413  csbov123  7474  elovmporab1w  7679  elovmporab1  7680  el2mpocsbcl  8108  mposn  8126  mpocurryvald  8293  fvmpocurryd  8294  eqerlem  8778  qliftfuns  8842  boxcutc  8979  iunfi  9380  wdom2d  9617  summolem2a  15747  zsum  15750  fsum  15752  sumsnf  15775  sumsns  15782  fsum2dlem  15802  fsumcom2  15806  fsumshftm  15813  fsum0diag2  15815  fsumrlim  15843  fsumo1  15844  fsumiun  15853  prodmolem2a  15966  prodsn  15994  prodsnf  15996  fprodm1s  16002  fprodp1s  16003  prodsns  16004  fprod2dlem  16012  fprodcom2  16016  pcmptdvds  16927  gsummpt1n0  19997  telgsumfzslem  20020  telgsumfzs  20021  psrass1lem  21969  coe1fzgsumdlem  22322  gsummoncoe1  22327  evl1gsumdlem  22375  madugsum  22664  fiuncmp  23427  elmptrab  23850  ovolfiniun  25549  finiunmbl  25592  volfiniun  25595  iundisj  25596  iundisj2  25597  iunmbl  25601  itgfsum  25876  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  itgsubstlem  26103  itgsubst  26104  rlimcnp2  27023  fsumdvdscom  27242  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  fsumvma  27271  dchrisumlem2  27548  ifeqeqx  32562  disji2f  32596  disjorsf  32599  disjif2  32600  disjabrex  32601  disjabrexf  32602  disjxpin  32607  iundisjf  32608  iundisj2f  32609  disjunsn  32613  aciunf1lem  32678  funcnv4mpt  32685  iundisjfi  32803  iundisj2fi  32804  fsumiunle  32835  gsummpt2co  33033  itgeq12i  36187  weiunfrlem  36446  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  finixpnum  37591  poimirlem24  37630  poimirlem26  37632  csbeq12  38144  fsumshftd  38933  cdlemk54  40940  evl1gprodd  42098  idomnnzgmulnz  42114  deg1gprod  42121  mzpsubst  42735  rabdiophlem2  42789  elnn0rabdioph  42790  dvdsrabdioph  42797  fphpd  42803  monotuz  42929  oddcomabszz  42932  fnwe2lem3  43040  flcidc  43158  sumsnd  44963  disjf1  45125  disjrnmpt2  45130  climinf2mpt  45669  climinfmpt  45670  dvnmptdivc  45893  dvmptfprod  45900  fourierdlem103  46164  fourierdlem104  46165  csbafv12g  47086  csbaovg  47129  csbafv212g  47168  fargshiftfva  47367