Theorem csbeq1 3856

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

Syntax hints:   → wi 4   = wceq 1561   ∈ wcel 2143  {cab 2741  [wsbc 3745  ⦋csb 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-sbc 3746  df-csb 3854

This theorem is referenced by:  csbeq1d  3857  csbeq1a  3867  csbconstg  3872  csbiebg  3885  cbvrabcsfw  3894  cbvralcsf  3895  cbvreucsf  3897  cbvrabcsf  3898  sbcnestgfw  4376  sbcnestgf  4381  csbun  4396  csbin  4397  csbdif  4480  csbif  4539  disjors  5084  disjxiun  5098  sbcbr123  5155  csbopab  5527  csbopabw  5528  pofun  5574  csbima12  6068  csbcog  6284  csbiota  6514  fvmpt2f  6976  fvmpts  6979  fvmpt2i  6986  fvmptex  6990  elfvmptrab1w  7003  elfvmptrab1  7004  fmptcof  7112  fmptcos  7113  fliftfuns  7298  csbriota  7368  riotaeqimp  7379  csbov123  7440  elovmporab1w  7643  elovmporab1  7644  el2mpocsbcl  8064  mposn  8082  mpocurryvald  8250  fvmpocurryd  8251  eqerlem  8714  qliftfuns  8786  boxcutc  8923  iunfi  9284  wdom2d  9526  summolem2a  15752  zsum  15755  fsum  15757  sumsnf  15780  sumsns  15787  fsum2dlem  15807  fsumcom2  15811  fsumshftm  15818  fsum0diag2  15820  fsumrlim  15849  fsumo1  15850  fsumiun  15859  prodmolem2a  15974  prodsn  16002  prodsnf  16004  fprodm1s  16010  fprodp1s  16011  prodsns  16012  fprod2dlem  16020  fprodcom2  16024  pcmptdvds  16940  gsummpt1n0  20015  telgsumfzslem  20038  telgsumfzs  20039  psrass1lem  21992  coe1fzgsumdlem  22373  gsummoncoe1  22378  evl1gsumdlem  22426  madugsum  22710  fiuncmp  23471  elmptrab  23894  ovolfiniun  25570  finiunmbl  25613  volfiniun  25616  iundisj  25617  iundisj2  25618  iunmbl  25622  itgfsum  25896  dvfsumle  26090  dvfsumabs  26092  dvfsumlem2  26096  dvfsumlem3  26097  dvfsumlem4  26098  dvfsum2  26103  itgsubstlem  26117  itgsubst  26118  rlimcnp2  27038  fsumdvdscom  27256  fsumdvdsmul  27266  fsumvma  27284  dchrisumlem2  27561  ifeqeqx  32747  disji2f  32783  disjorsf  32786  disjif2  32787  disjabrex  32788  disjabrexf  32789  disjxpin  32794  iundisjf  32795  iundisj2f  32796  disjunsn  32800  aciunf1lem  32870  funcnv4mpt  32876  iundisjfi  33004  iundisj2fi  33005  fsumiunle  33037  gsummpt2co  33234  itgeq12i  36571  weiunfrlem  36829  weiunpo  36830  weiunso  36831  weiunfr  36832  weiunse  36833  csbttc  36874  finixpnum  38109  poimirlem24  38148  poimirlem26  38150  csbeq12  38662  fsumshftd  39581  cdlemk54  41587  evl1gprodd  42739  idomnnzgmulnz  42755  deg1gprod  42762  mzpsubst  43334  rabdiophlem2  43384  elnn0rabdioph  43385  dvdsrabdioph  43392  fphpd  43398  monotuz  43523  oddcomabszz  43526  fnwe2lem3  43634  flcidc  43752  sumsnd  45597  disjf1  45752  disjrnmpt2  45757  climinf2mpt  46279  climinfmpt  46280  dvnmptdivc  46503  dvmptfprod  46510  fourierdlem103  46774  fourierdlem104  46775  csbafv12g  47722  csbaovg  47765  csbafv212g  47804  fargshiftfva  48040