Theorem csbeq1 3853

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3741  ⦋csb 3850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbeq1d  3854  csbeq1a  3864  csbconstg  3869  csbiebg  3882  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbcnestgfw  4374  sbcnestgf  4379  csbun  4394  csbin  4395  csbdif  4479  csbif  4538  disjors  5082  disjxiun  5096  sbcbr123  5153  csbopab  5504  csbopabgALT  5505  pofun  5551  csbima12  6039  csbcog  6256  csbiota  6486  fvmpt2f  6943  fvmpts  6946  fvmpt2i  6953  fvmptex  6957  elfvmptrab1w  6970  elfvmptrab1  6971  fmptcof  7078  fmptcos  7079  fliftfuns  7263  csbriota  7333  riotaeqimp  7344  csbov123  7405  elovmporab1w  7608  elovmporab1  7609  el2mpocsbcl  8030  mposn  8048  mpocurryvald  8215  fvmpocurryd  8216  eqerlem  8674  qliftfuns  8746  boxcutc  8884  iunfi  9248  wdom2d  9490  summolem2a  15643  zsum  15646  fsum  15648  sumsnf  15671  sumsns  15678  fsum2dlem  15698  fsumcom2  15702  fsumshftm  15709  fsum0diag2  15711  fsumrlim  15739  fsumo1  15740  fsumiun  15749  prodmolem2a  15862  prodsn  15890  prodsnf  15892  fprodm1s  15898  fprodp1s  15899  prodsns  15900  fprod2dlem  15908  fprodcom2  15912  pcmptdvds  16827  gsummpt1n0  19899  telgsumfzslem  19922  telgsumfzs  19923  psrass1lem  21893  coe1fzgsumdlem  22252  gsummoncoe1  22257  evl1gsumdlem  22305  madugsum  22592  fiuncmp  23353  elmptrab  23776  ovolfiniun  25463  finiunmbl  25506  volfiniun  25509  iundisj  25510  iundisj2  25511  iunmbl  25515  itgfsum  25789  dvfsumle  25987  dvfsumleOLD  25988  dvfsumabs  25990  dvfsumlem2  25994  dvfsumlem2OLD  25995  dvfsumlem3  25996  dvfsumlem4  25997  dvfsum2  26002  itgsubstlem  26016  itgsubst  26017  rlimcnp2  26937  fsumdvdscom  27156  fsumdvdsmul  27166  fsumdvdsmulOLD  27168  fsumvma  27185  dchrisumlem2  27462  ifeqeqx  32621  disji2f  32656  disjorsf  32659  disjif2  32660  disjabrex  32661  disjabrexf  32662  disjxpin  32667  iundisjf  32668  iundisj2f  32669  disjunsn  32673  aciunf1lem  32744  funcnv4mpt  32750  iundisjfi  32879  iundisj2fi  32880  fsumiunle  32913  gsummpt2co  33134  itgeq12i  36413  weiunfrlem  36671  weiunpo  36672  weiunso  36673  weiunfr  36674  weiunse  36675  finixpnum  37819  poimirlem24  37858  poimirlem26  37860  csbeq12  38372  fsumshftd  39291  cdlemk54  41297  evl1gprodd  42450  idomnnzgmulnz  42466  deg1gprod  42473  mzpsubst  43068  rabdiophlem2  43122  elnn0rabdioph  43123  dvdsrabdioph  43130  fphpd  43136  monotuz  43261  oddcomabszz  43264  fnwe2lem3  43372  flcidc  43490  sumsnd  45349  disjf1  45505  disjrnmpt2  45510  climinf2mpt  46035  climinfmpt  46036  dvnmptdivc  46259  dvmptfprod  46266  fourierdlem103  46530  fourierdlem104  46531  csbafv12g  47460  csbaovg  47503  csbafv212g  47542  fargshiftfva  47766