Theorem csbeq1 3892

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099  {cab 2704  [wsbc 3774  ⦋csb 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-sbc 3775  df-csb 3890

This theorem is referenced by:  csbeq1d  3893  csbeq1a  3903  csbconstg  3908  csbiebg  3922  cbvrabcsfw  3933  cbvralcsf  3934  cbvreucsf  3936  cbvrabcsf  3937  sbcnestgfw  4414  sbcnestgf  4419  csbun  4434  csbin  4435  csbdif  4523  csbif  4581  disjors  5123  disjxiun  5139  sbcbr123  5196  csbopab  5551  csbopabgALT  5552  pofun  5602  csbima12  6076  csbcog  6295  csbiota  6535  fvmpt2f  7000  fvmpts  7002  fvmpt2i  7009  fvmptex  7013  elfvmptrab1w  7026  elfvmptrab1  7027  fmptcof  7133  fmptcos  7134  fliftfuns  7316  csbriota  7386  riotaeqimp  7397  csbov123  7456  elovmporab1w  7662  elovmporab1  7663  el2mpocsbcl  8084  mposn  8102  mpocurryvald  8269  fvmpocurryd  8270  eqerlem  8752  qliftfuns  8814  boxcutc  8951  iunfi  9356  wdom2d  9595  summolem2a  15685  zsum  15688  fsum  15690  sumsnf  15713  sumsns  15720  fsum2dlem  15740  fsumcom2  15744  fsumshftm  15751  fsum0diag2  15753  fsumrlim  15781  fsumo1  15782  fsumiun  15791  prodmolem2a  15902  prodsn  15930  prodsnf  15932  fprodm1s  15938  fprodp1s  15939  prodsns  15940  fprod2dlem  15948  fprodcom2  15952  pcmptdvds  16854  gsummpt1n0  19911  telgsumfzslem  19934  telgsumfzs  19935  psrass1lemOLD  21861  psrass1lem  21864  coe1fzgsumdlem  22209  gsummoncoe1  22214  evl1gsumdlem  22262  madugsum  22532  fiuncmp  23295  elmptrab  23718  ovolfiniun  25417  finiunmbl  25460  volfiniun  25463  iundisj  25464  iundisj2  25465  iunmbl  25469  itgfsum  25743  dvfsumle  25941  dvfsumleOLD  25942  dvfsumabs  25944  dvfsumlem2  25948  dvfsumlem2OLD  25949  dvfsumlem3  25950  dvfsumlem4  25951  dvfsum2  25956  itgsubstlem  25970  itgsubst  25971  rlimcnp2  26885  fsumdvdscom  27104  fsumdvdsmul  27114  fsumdvdsmulOLD  27116  fsumvma  27133  dchrisumlem2  27410  ifeqeqx  32318  disji2f  32352  disjorsf  32355  disjif2  32356  disjabrex  32357  disjabrexf  32358  disjxpin  32363  iundisjf  32364  iundisj2f  32365  disjunsn  32369  aciunf1lem  32431  funcnv4mpt  32438  iundisjfi  32548  iundisj2fi  32549  fsumiunle  32574  gsummpt2co  32740  finixpnum  37013  poimirlem24  37052  poimirlem26  37054  csbeq12  37566  fsumshftd  38361  cdlemk54  40368  evl1gprodd  41521  idomnnzgmulnz  41536  deg1gprod  41544  mzpsubst  42090  rabdiophlem2  42144  elnn0rabdioph  42145  dvdsrabdioph  42152  fphpd  42158  monotuz  42284  oddcomabszz  42287  fnwe2lem3  42398  flcidc  42520  sumsnd  44311  disjf1  44479  disjrnmpt2  44484  climinf2mpt  45025  climinfmpt  45026  dvnmptdivc  45249  fourierdlem103  45520  fourierdlem104  45521  csbafv12g  46440  csbaovg  46483  csbafv212g  46522  fargshiftfva  46706