Theorem csbeq1 3896

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2107  {cab 2710  [wsbc 3777  ⦋csb 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3778  df-csb 3894

This theorem is referenced by:  csbeq1d  3897  csbeq1a  3907  csbconstg  3912  csbiebg  3926  cbvrabcsfw  3937  cbvralcsf  3938  cbvreucsf  3940  cbvrabcsf  3941  sbcnestgfw  4418  sbcnestgf  4423  csbun  4438  csbin  4439  csbdif  4527  csbif  4585  disjors  5129  disjxiun  5145  sbcbr123  5202  csbopab  5555  csbopabgALT  5556  pofun  5606  csbima12  6076  csbcog  6294  csbiota  6534  fvmpt2f  6997  fvmpts  6999  fvmpt2i  7006  fvmptex  7010  elfvmptrab1w  7022  elfvmptrab1  7023  fmptcof  7125  fmptcos  7126  fliftfuns  7308  csbriota  7378  riotaeqimp  7389  csbov123  7448  elovmporab1w  7650  elovmporab1  7651  el2mpocsbcl  8068  mposn  8086  mpocurryvald  8252  fvmpocurryd  8253  eqerlem  8734  qliftfuns  8795  boxcutc  8932  iunfi  9337  wdom2d  9572  summolem2a  15658  zsum  15661  fsum  15663  sumsnf  15686  sumsns  15693  fsum2dlem  15713  fsumcom2  15717  fsumshftm  15724  fsum0diag2  15726  fsumrlim  15754  fsumo1  15755  fsumiun  15764  prodmolem2a  15875  prodsn  15903  prodsnf  15905  fprodm1s  15911  fprodp1s  15912  prodsns  15913  fprod2dlem  15921  fprodcom2  15925  pcmptdvds  16824  gsummpt1n0  19828  telgsumfzslem  19851  telgsumfzs  19852  psrass1lemOLD  21485  psrass1lem  21488  coe1fzgsumdlem  21817  gsummoncoe1  21820  evl1gsumdlem  21867  madugsum  22137  fiuncmp  22900  elmptrab  23323  ovolfiniun  25010  finiunmbl  25053  volfiniun  25056  iundisj  25057  iundisj2  25058  iunmbl  25062  itgfsum  25336  dvfsumle  25530  dvfsumabs  25532  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsum2  25543  itgsubstlem  25557  itgsubst  25558  rlimcnp2  26461  fsumdvdscom  26679  fsumdvdsmul  26689  fsumvma  26706  dchrisumlem2  26983  ifeqeqx  31762  disji2f  31796  disjorsf  31799  disjif2  31800  disjabrex  31801  disjabrexf  31802  disjxpin  31807  iundisjf  31808  iundisj2f  31809  disjunsn  31813  aciunf1lem  31875  funcnv4mpt  31882  iundisjfi  31995  iundisj2fi  31996  fsumiunle  32023  gsummpt2co  32188  gg-dvfsumle  35171  gg-dvfsumlem2  35172  finixpnum  36462  poimirlem24  36501  poimirlem26  36503  csbeq12  37015  fsumshftd  37811  cdlemk54  39818  mzpsubst  41472  rabdiophlem2  41526  elnn0rabdioph  41527  dvdsrabdioph  41534  fphpd  41540  monotuz  41666  oddcomabszz  41669  fnwe2lem3  41780  flcidc  41902  sumsnd  43696  disjf1  43866  disjrnmpt2  43872  climinf2mpt  44417  climinfmpt  44418  dvnmptdivc  44641  fourierdlem103  44912  fourierdlem104  44913  csbafv12g  45832  csbaovg  45875  csbafv212g  45914  fargshiftfva  46098