Theorem csbeq1 3864

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

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {cab 2747  [wsbc 3753  ⦋csb 3861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754  df-csb 3862

This theorem is referenced by:  csbeq1d  3865  csbeq1a  3875  csbconstg  3880  csbiebg  3893  cbvrabcsfw  3902  cbvralcsf  3903  cbvreucsf  3905  cbvrabcsf  3906  sbcnestgfw  4392  sbcnestgf  4397  csbun  4412  csbin  4413  csbdif  4491  csbif  4550  disjors  5096  disjxiun  5110  sbcbr123  5169  csbopab  5541  csbopabw  5542  pofun  5588  csbima12  6082  csbcog  6299  csbiota  6530  fvmpt2f  6991  fvmpts  6994  fvmpt2i  7001  fvmptex  7005  elfvmptrab1w  7018  elfvmptrab1  7019  fmptcof  7127  fmptcos  7128  fliftfuns  7313  csbriota  7383  riotaeqimp  7394  csbov123  7455  elovmporab1w  7658  elovmporab1  7659  el2mpocsbcl  8080  mposn  8098  mpocurryvald  8266  fvmpocurryd  8267  eqerlem  8730  qliftfuns  8802  boxcutc  8939  iunfi  9300  wdom2d  9542  summolem2a  15766  zsum  15769  fsum  15771  sumsnf  15794  sumsns  15801  fsum2dlem  15821  fsumcom2  15825  fsumshftm  15832  fsum0diag2  15834  fsumrlim  15863  fsumo1  15864  fsumiun  15873  prodmolem2a  15988  prodsn  16016  prodsnf  16018  fprodm1s  16024  fprodp1s  16025  prodsns  16026  fprod2dlem  16034  fprodcom2  16038  pcmptdvds  16954  gsummpt1n0  20035  telgsumfzslem  20058  telgsumfzs  20059  psrass1lem  22052  coe1fzgsumdlem  22432  gsummoncoe1  22437  evl1gsumdlem  22485  madugsum  22769  fiuncmp  23530  elmptrab  23953  ovolfiniun  25629  finiunmbl  25672  volfiniun  25675  iundisj  25676  iundisj2  25677  iunmbl  25681  itgfsum  25955  dvfsumle  26149  dvfsumabs  26151  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumlem4  26157  dvfsum2  26162  itgsubstlem  26176  itgsubst  26177  rlimcnp2  27097  fsumdvdscom  27315  fsumdvdsmul  27325  fsumvma  27343  dchrisumlem2  27620  ifeqeqx  32829  disji2f  32863  disjorsf  32866  disjif2  32867  disjabrex  32868  disjabrexf  32869  disjxpin  32874  iundisjf  32875  iundisj2f  32876  disjunsn  32880  aciunf1lem  32948  funcnv4mpt  32954  iundisjfi  33082  iundisj2fi  33083  fsumiunle  33114  gsummpt2co  33309  itgeq12i  36641  weiunfrlem  36898  weiunpo  36899  weiunso  36900  weiunfr  36901  weiunse  36902  csbttc  36943  finixpnum  38178  poimirlem24  38217  poimirlem26  38219  csbeq12  38731  fsumshftd  39650  cdlemk54  41656  evl1gprodd  42808  idomnnzgmulnz  42824  deg1gprod  42831  mzpsubst  43405  rabdiophlem2  43455  elnn0rabdioph  43456  dvdsrabdioph  43463  fphpd  43469  monotuz  43594  oddcomabszz  43597  fnwe2lem3  43705  flcidc  43823  sumsnd  45672  disjf1  45827  disjrnmpt2  45832  climinf2mpt  46354  climinfmpt  46355  dvnmptdivc  46578  dvmptfprod  46585  fourierdlem103  46849  fourierdlem104  46850  csbafv12g  47797  csbaovg  47840  csbafv212g  47879  fargshiftfva  48115