Theorem csbeq1 3853

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  [wsbc 3741  ⦋csb 3850

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sbc 3742  df-csb 3851

This theorem is referenced by:  csbeq1d  3854  csbeq1a  3864  csbconstg  3869  csbiebg  3882  cbvrabcsfw  3891  cbvralcsf  3892  cbvreucsf  3894  cbvrabcsf  3895  sbcnestgfw  4374  sbcnestgf  4379  csbun  4394  csbin  4395  csbdif  4479  csbif  4538  disjors  5082  disjxiun  5096  sbcbr123  5153  csbopab  5504  csbopabgALT  5505  pofun  5551  csbima12  6039  csbcog  6256  csbiota  6486  fvmpt2f  6943  fvmpts  6946  fvmpt2i  6953  fvmptex  6957  elfvmptrab1w  6970  elfvmptrab1  6971  fmptcof  7077  fmptcos  7078  fliftfuns  7262  csbriota  7332  riotaeqimp  7343  csbov123  7404  elovmporab1w  7607  elovmporab1  7608  el2mpocsbcl  8029  mposn  8047  mpocurryvald  8214  fvmpocurryd  8215  eqerlem  8673  qliftfuns  8745  boxcutc  8883  iunfi  9247  wdom2d  9489  summolem2a  15642  zsum  15645  fsum  15647  sumsnf  15670  sumsns  15677  fsum2dlem  15697  fsumcom2  15701  fsumshftm  15708  fsum0diag2  15710  fsumrlim  15738  fsumo1  15739  fsumiun  15748  prodmolem2a  15861  prodsn  15889  prodsnf  15891  fprodm1s  15897  fprodp1s  15898  prodsns  15899  fprod2dlem  15907  fprodcom2  15911  pcmptdvds  16826  gsummpt1n0  19898  telgsumfzslem  19921  telgsumfzs  19922  psrass1lem  21892  coe1fzgsumdlem  22251  gsummoncoe1  22256  evl1gsumdlem  22304  madugsum  22591  fiuncmp  23352  elmptrab  23775  ovolfiniun  25462  finiunmbl  25505  volfiniun  25508  iundisj  25509  iundisj2  25510  iunmbl  25514  itgfsum  25788  dvfsumle  25986  dvfsumleOLD  25987  dvfsumabs  25989  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  itgsubstlem  26015  itgsubst  26016  rlimcnp2  26936  fsumdvdscom  27155  fsumdvdsmul  27165  fsumdvdsmulOLD  27167  fsumvma  27184  dchrisumlem2  27461  ifeqeqx  32599  disji2f  32634  disjorsf  32637  disjif2  32638  disjabrex  32639  disjabrexf  32640  disjxpin  32645  iundisjf  32646  iundisj2f  32647  disjunsn  32651  aciunf1lem  32722  funcnv4mpt  32728  iundisjfi  32857  iundisj2fi  32858  fsumiunle  32891  gsummpt2co  33112  itgeq12i  36381  weiunfrlem  36639  weiunpo  36640  weiunso  36641  weiunfr  36642  weiunse  36643  finixpnum  37777  poimirlem24  37816  poimirlem26  37818  csbeq12  38330  fsumshftd  39249  cdlemk54  41255  evl1gprodd  42408  idomnnzgmulnz  42424  deg1gprod  42431  mzpsubst  43026  rabdiophlem2  43080  elnn0rabdioph  43081  dvdsrabdioph  43088  fphpd  43094  monotuz  43219  oddcomabszz  43222  fnwe2lem3  43330  flcidc  43448  sumsnd  45307  disjf1  45463  disjrnmpt2  45468  climinf2mpt  45994  climinfmpt  45995  dvnmptdivc  46218  dvmptfprod  46225  fourierdlem103  46489  fourierdlem104  46490  csbafv12g  47419  csbaovg  47462  csbafv212g  47501  fargshiftfva  47725