Theorem csbeq1 3846

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

Syntax hints:   → wi 4   = wceq 1550   ∈ wcel 2132  {cab 2730  [wsbc 3735  ⦋csb 3843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-sbc 3736  df-csb 3844

This theorem is referenced by:  csbeq1d  3847  csbeq1a  3857  csbconstg  3862  csbiebg  3875  cbvrabcsfw  3884  cbvralcsf  3885  cbvreucsf  3887  cbvrabcsf  3888  sbcnestgfw  4365  sbcnestgf  4370  csbun  4385  csbin  4386  csbdif  4469  csbif  4528  disjors  5073  disjxiun  5087  sbcbr123  5144  csbopab  5515  csbopabw  5516  pofun  5562  csbima12  6054  csbcog  6269  csbiota  6499  fvmpt2f  6961  fvmpts  6964  fvmpt2i  6971  fvmptex  6975  elfvmptrab1w  6988  elfvmptrab1  6989  fmptcof  7097  fmptcos  7098  fliftfuns  7283  csbriota  7353  riotaeqimp  7364  csbov123  7425  elovmporab1w  7628  elovmporab1  7629  el2mpocsbcl  8048  mposn  8066  mpocurryvald  8234  fvmpocurryd  8235  eqerlem  8698  qliftfuns  8770  boxcutc  8908  iunfi  9272  wdom2d  9514  summolem2a  15714  zsum  15717  fsum  15719  sumsnf  15742  sumsns  15749  fsum2dlem  15769  fsumcom2  15773  fsumshftm  15780  fsum0diag2  15782  fsumrlim  15811  fsumo1  15812  fsumiun  15821  prodmolem2a  15936  prodsn  15964  prodsnf  15966  fprodm1s  15972  fprodp1s  15973  prodsns  15974  fprod2dlem  15982  fprodcom2  15986  pcmptdvds  16902  gsummpt1n0  19977  telgsumfzslem  20000  telgsumfzs  20001  psrass1lem  21954  coe1fzgsumdlem  22335  gsummoncoe1  22340  evl1gsumdlem  22388  madugsum  22672  fiuncmp  23433  elmptrab  23856  ovolfiniun  25532  finiunmbl  25575  volfiniun  25578  iundisj  25579  iundisj2  25580  iunmbl  25584  itgfsum  25858  dvfsumle  26052  dvfsumabs  26054  dvfsumlem2  26058  dvfsumlem3  26059  dvfsumlem4  26060  dvfsum2  26065  itgsubstlem  26079  itgsubst  26080  rlimcnp2  26997  fsumdvdscom  27215  fsumdvdsmul  27225  fsumvma  27243  dchrisumlem2  27520  ifeqeqx  32679  disji2f  32715  disjorsf  32718  disjif2  32719  disjabrex  32720  disjabrexf  32721  disjxpin  32726  iundisjf  32727  iundisj2f  32728  disjunsn  32732  aciunf1lem  32803  funcnv4mpt  32809  iundisjfi  32937  iundisj2fi  32938  fsumiunle  32970  gsummpt2co  33178  itgeq12i  36504  weiunfrlem  36762  weiunpo  36763  weiunso  36764  weiunfr  36765  weiunse  36766  csbttc  36807  finixpnum  38042  poimirlem24  38081  poimirlem26  38083  csbeq12  38595  fsumshftd  39514  cdlemk54  41520  evl1gprodd  42672  idomnnzgmulnz  42688  deg1gprod  42695  mzpsubst  43267  rabdiophlem2  43317  elnn0rabdioph  43318  dvdsrabdioph  43325  fphpd  43331  monotuz  43456  oddcomabszz  43459  fnwe2lem3  43567  flcidc  43685  sumsnd  45544  disjf1  45699  disjrnmpt2  45704  climinf2mpt  46226  climinfmpt  46227  dvnmptdivc  46450  dvmptfprod  46457  fourierdlem103  46721  fourierdlem104  46722  csbafv12g  47669  csbaovg  47712  csbafv212g  47751  fargshiftfva  47987