Theorem csbeq1 3893

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  {cab 2702  [wsbc 3774  ⦋csb 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sbc 3775  df-csb 3891

This theorem is referenced by:  csbeq1d  3894  csbeq1a  3904  csbconstg  3909  csbiebg  3923  cbvrabcsfw  3934  cbvralcsf  3935  cbvreucsf  3937  cbvrabcsf  3938  sbcnestgfw  4419  sbcnestgf  4424  csbun  4439  csbin  4440  csbdif  4528  csbif  4586  disjors  5129  disjxiun  5145  sbcbr123  5202  csbopab  5556  csbopabgALT  5557  pofun  5607  csbima12  6082  csbcog  6301  csbiota  6540  fvmpt2f  7003  fvmpts  7005  fvmpt2i  7012  fvmptex  7016  elfvmptrab1w  7029  elfvmptrab1  7030  fmptcof  7137  fmptcos  7138  fliftfuns  7319  csbriota  7389  riotaeqimp  7400  csbov123  7460  elovmporab1w  7666  elovmporab1  7667  el2mpocsbcl  8088  mposn  8106  mpocurryvald  8274  fvmpocurryd  8275  eqerlem  8757  qliftfuns  8821  boxcutc  8958  iunfi  9364  wdom2d  9603  summolem2a  15693  zsum  15696  fsum  15698  sumsnf  15721  sumsns  15728  fsum2dlem  15748  fsumcom2  15752  fsumshftm  15759  fsum0diag2  15761  fsumrlim  15789  fsumo1  15790  fsumiun  15799  prodmolem2a  15910  prodsn  15938  prodsnf  15940  fprodm1s  15946  fprodp1s  15947  prodsns  15948  fprod2dlem  15956  fprodcom2  15960  pcmptdvds  16862  gsummpt1n0  19924  telgsumfzslem  19947  telgsumfzs  19948  psrass1lemOLD  21878  psrass1lem  21881  coe1fzgsumdlem  22231  gsummoncoe1  22236  evl1gsumdlem  22284  madugsum  22575  fiuncmp  23338  elmptrab  23761  ovolfiniun  25460  finiunmbl  25503  volfiniun  25506  iundisj  25507  iundisj2  25508  iunmbl  25512  itgfsum  25786  dvfsumle  25984  dvfsumleOLD  25985  dvfsumabs  25987  dvfsumlem2  25991  dvfsumlem2OLD  25992  dvfsumlem3  25993  dvfsumlem4  25994  dvfsum2  25999  itgsubstlem  26013  itgsubst  26014  rlimcnp2  26928  fsumdvdscom  27147  fsumdvdsmul  27157  fsumdvdsmulOLD  27159  fsumvma  27176  dchrisumlem2  27453  ifeqeqx  32390  disji2f  32424  disjorsf  32427  disjif2  32428  disjabrex  32429  disjabrexf  32430  disjxpin  32435  iundisjf  32436  iundisj2f  32437  disjunsn  32441  aciunf1lem  32505  funcnv4mpt  32512  iundisjfi  32621  iundisj2fi  32622  fsumiunle  32649  gsummpt2co  32819  finixpnum  37148  poimirlem24  37187  poimirlem26  37189  csbeq12  37701  fsumshftd  38493  cdlemk54  40500  evl1gprodd  41657  idomnnzgmulnz  41673  deg1gprod  41681  mzpsubst  42233  rabdiophlem2  42287  elnn0rabdioph  42288  dvdsrabdioph  42295  fphpd  42301  monotuz  42427  oddcomabszz  42430  fnwe2lem3  42541  flcidc  42663  sumsnd  44453  disjf1  44620  disjrnmpt2  44625  climinf2mpt  45165  climinfmpt  45166  dvnmptdivc  45389  fourierdlem103  45660  fourierdlem104  45661  csbafv12g  46580  csbaovg  46623  csbafv212g  46662  fargshiftfva  46846