Theorem csbeq1 3865

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 2795	. 2 ⊢ (𝐴 = 𝐵 → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶} = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶})
3		df-csb 3863	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐶}
4		df-csb 3863	. 2 ⊢ ⦋𝐵 / 𝑥⦌𝐶 = {𝑦 ∣ [𝐵 / 𝑥]𝑦 ∈ 𝐶}
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⦋𝐴 / 𝑥⦌𝐶 = ⦋𝐵 / 𝑥⦌𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  [wsbc 3753  ⦋csb 3862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754  df-csb 3863

This theorem is referenced by:  csbeq1d  3866  csbeq1a  3876  csbconstg  3881  csbiebg  3894  cbvrabcsfw  3903  cbvralcsf  3904  cbvreucsf  3906  cbvrabcsf  3907  sbcnestgfw  4384  sbcnestgf  4389  csbun  4404  csbin  4405  csbdif  4487  csbif  4546  disjors  5090  disjxiun  5104  sbcbr123  5161  csbopab  5515  csbopabgALT  5516  pofun  5564  csbima12  6050  csbcog  6270  csbiota  6504  fvmpt2f  6969  fvmpts  6971  fvmpt2i  6978  fvmptex  6982  elfvmptrab1w  6995  elfvmptrab1  6996  fmptcof  7102  fmptcos  7103  fliftfuns  7289  csbriota  7359  riotaeqimp  7370  csbov123  7431  elovmporab1w  7636  elovmporab1  7637  el2mpocsbcl  8064  mposn  8082  mpocurryvald  8249  fvmpocurryd  8250  eqerlem  8706  qliftfuns  8777  boxcutc  8914  iunfi  9294  wdom2d  9533  summolem2a  15681  zsum  15684  fsum  15686  sumsnf  15709  sumsns  15716  fsum2dlem  15736  fsumcom2  15740  fsumshftm  15747  fsum0diag2  15749  fsumrlim  15777  fsumo1  15778  fsumiun  15787  prodmolem2a  15900  prodsn  15928  prodsnf  15930  fprodm1s  15936  fprodp1s  15937  prodsns  15938  fprod2dlem  15946  fprodcom2  15950  pcmptdvds  16865  gsummpt1n0  19895  telgsumfzslem  19918  telgsumfzs  19919  psrass1lem  21841  coe1fzgsumdlem  22190  gsummoncoe1  22195  evl1gsumdlem  22243  madugsum  22530  fiuncmp  23291  elmptrab  23714  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  iundisj  25449  iundisj2  25450  iunmbl  25454  itgfsum  25728  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  itgsubstlem  25955  itgsubst  25956  rlimcnp2  26876  fsumdvdscom  27095  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  fsumvma  27124  dchrisumlem2  27401  ifeqeqx  32471  disji2f  32506  disjorsf  32509  disjif2  32510  disjabrex  32511  disjabrexf  32512  disjxpin  32517  iundisjf  32518  iundisj2f  32519  disjunsn  32523  aciunf1lem  32586  funcnv4mpt  32593  iundisjfi  32719  iundisj2fi  32720  fsumiunle  32754  gsummpt2co  32988  itgeq12i  36194  weiunfrlem  36452  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  finixpnum  37599  poimirlem24  37638  poimirlem26  37640  csbeq12  38152  fsumshftd  38945  cdlemk54  40952  evl1gprodd  42105  idomnnzgmulnz  42121  deg1gprod  42128  mzpsubst  42736  rabdiophlem2  42790  elnn0rabdioph  42791  dvdsrabdioph  42798  fphpd  42804  monotuz  42930  oddcomabszz  42933  fnwe2lem3  43041  flcidc  43159  sumsnd  45020  disjf1  45177  disjrnmpt2  45182  climinf2mpt  45712  climinfmpt  45713  dvnmptdivc  45936  dvmptfprod  45943  fourierdlem103  46207  fourierdlem104  46208  csbafv12g  47138  csbaovg  47181  csbafv212g  47220  fargshiftfva  47444