Theorem csbeq1 3836

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2713  [wsbc 3725  ⦋csb 3833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-sbc 3726  df-csb 3834

This theorem is referenced by:  csbeq1d  3837  csbeq1a  3847  csbconstg  3852  csbiebg  3865  cbvrabcsfw  3874  cbvralcsf  3875  cbvreucsf  3877  cbvrabcsf  3878  sbcnestgfw  4351  sbcnestgf  4356  csbun  4371  csbin  4372  csbdif  4455  csbif  4514  disjors  5057  disjxiun  5071  sbcbr123  5128  csbopab  5499  csbopabgALT  5500  pofun  5546  csbima12  6033  csbcog  6250  csbiota  6480  fvmpt2f  6937  fvmpts  6940  fvmpt2i  6947  fvmptex  6951  elfvmptrab1w  6964  elfvmptrab1  6965  fmptcof  7072  fmptcos  7073  fliftfuns  7258  csbriota  7328  riotaeqimp  7339  csbov123  7400  elovmporab1w  7603  elovmporab1  7604  el2mpocsbcl  8024  mposn  8042  mpocurryvald  8209  fvmpocurryd  8210  eqerlem  8668  qliftfuns  8740  boxcutc  8878  iunfi  9242  wdom2d  9484  summolem2a  15666  zsum  15669  fsum  15671  sumsnf  15694  sumsns  15701  fsum2dlem  15721  fsumcom2  15725  fsumshftm  15732  fsum0diag2  15734  fsumrlim  15763  fsumo1  15764  fsumiun  15773  prodmolem2a  15888  prodsn  15916  prodsnf  15918  fprodm1s  15924  fprodp1s  15925  prodsns  15926  fprod2dlem  15934  fprodcom2  15938  pcmptdvds  16854  gsummpt1n0  19929  telgsumfzslem  19952  telgsumfzs  19953  psrass1lem  21901  coe1fzgsumdlem  22256  gsummoncoe1  22261  evl1gsumdlem  22309  madugsum  22596  fiuncmp  23357  elmptrab  23780  ovolfiniun  25456  finiunmbl  25499  volfiniun  25502  iundisj  25503  iundisj2  25504  iunmbl  25508  itgfsum  25782  dvfsumle  25976  dvfsumabs  25978  dvfsumlem2  25982  dvfsumlem3  25983  dvfsumlem4  25984  dvfsum2  25989  itgsubstlem  26003  itgsubst  26004  rlimcnp2  26918  fsumdvdscom  27136  fsumdvdsmul  27146  fsumvma  27164  dchrisumlem2  27441  ifeqeqx  32600  disji2f  32635  disjorsf  32638  disjif2  32639  disjabrex  32640  disjabrexf  32641  disjxpin  32646  iundisjf  32647  iundisj2f  32648  disjunsn  32652  aciunf1lem  32723  funcnv4mpt  32729  iundisjfi  32857  iundisj2fi  32858  fsumiunle  32890  gsummpt2co  33097  itgeq12i  36376  weiunfrlem  36634  weiunpo  36635  weiunso  36636  weiunfr  36637  weiunse  36638  csbttc  36679  finixpnum  37914  poimirlem24  37953  poimirlem26  37955  csbeq12  38467  fsumshftd  39386  cdlemk54  41392  evl1gprodd  42544  idomnnzgmulnz  42560  deg1gprod  42567  mzpsubst  43168  rabdiophlem2  43218  elnn0rabdioph  43219  dvdsrabdioph  43226  fphpd  43232  monotuz  43357  oddcomabszz  43360  fnwe2lem3  43468  flcidc  43586  sumsnd  45445  disjf1  45601  disjrnmpt2  45606  climinf2mpt  46130  climinfmpt  46131  dvnmptdivc  46354  dvmptfprod  46361  fourierdlem103  46625  fourierdlem104  46626  csbafv12g  47573  csbaovg  47616  csbafv212g  47655  fargshiftfva  47891