Theorem csbeq1 3784

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

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  {cab 2753  [wsbc 3676  ⦋csb 3781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-sbc 3677  df-csb 3782

This theorem is referenced by:  csbeq1d  3788  csbeq1a  3790  csbiebg  3806  cbvralcsf  3815  cbvreucsf  3817  cbvrabcsf  3818  sbcnestgf  4254  csbun  4269  csbin  4270  csbif  4400  disjors  4909  disjxiun  4923  sbcbr123  4980  csbopab  5291  csbopabgALT  5292  pofun  5340  csbima12  5785  csbiota  6179  fvmpt2f  6595  fvmpts  6597  fvmpt2i  6603  fvmptex  6607  elfvmptrab1  6619  fmptcof  6714  fmptcos  6715  fliftfuns  6889  csbriota  6948  riotaeqimp  6959  csbov123  7016  elovmporab1  7210  el2mpocsbcl  7587  mposn  7605  mpocurryvald  7738  fvmpocurryd  7739  eqerlem  8122  qliftfuns  8183  boxcutc  8301  iunfi  8606  wdom2d  8838  summolem2a  14931  zsum  14934  fsum  14936  sumsnf  14958  sumsns  14964  fsum2dlem  14984  fsumcom2  14988  fsumshftm  14995  fsum0diag2  14997  fsumrlim  15025  fsumo1  15026  fsumiun  15035  prodmolem2a  15147  prodsn  15175  prodsnf  15177  fprodm1s  15183  fprodp1s  15184  prodsns  15185  fprod2dlem  15193  fprodcom2  15197  pcmptdvds  16085  gsummpt1n0  18851  telgsumfzslem  18871  telgsumfzs  18872  psrass1lem  19884  coe1fzgsumdlem  20188  gsummoncoe1  20191  evl1gsumdlem  20237  madugsum  20972  fiuncmp  21732  elmptrab  22155  ovolfiniun  23821  finiunmbl  23864  volfiniun  23867  iundisj  23868  iundisj2  23869  iunmbl  23873  itgfsum  24146  dvfsumle  24337  dvfsumabs  24339  dvfsumlem2  24343  dvfsumlem3  24344  dvfsumlem4  24345  dvfsum2  24350  itgsubstlem  24364  itgsubst  24365  rlimcnp2  25262  fsumdvdscom  25480  fsumdvdsmul  25490  fsumvma  25507  dchrisumlem2  25784  ifeqeqx  30083  disji2f  30111  disjorsf  30114  disjif2  30115  disjabrex  30116  disjabrexf  30117  disjxpin  30122  iundisjf  30123  iundisj2f  30124  disjunsn  30128  aciunf1lem  30187  funcnv4mpt  30194  iundisjfi  30293  iundisj2fi  30294  fsumiunle  30316  gsummpt2co  30556  csbdif  34081  finixpnum  34351  poimirlem24  34390  poimirlem26  34392  csbeq12  34913  fsumshftd  35566  cdlemk54  37572  mzpsubst  38774  rabdiophlem2  38829  elnn0rabdioph  38830  dvdsrabdioph  38837  fphpd  38843  monotuz  38968  oddcomabszz  38971  fnwe2lem3  39082  flcidc  39204  csbcog  39391  sumsnd  40736  disjf1  40898  disjrnmpt2  40904  climinf2mpt  41456  climinfmpt  41457  dvnmptdivc  41683  fourierdlem103  41955  fourierdlem104  41956  csbafv12g  42772  csbaovg  42815  csbafv212g  42854  fargshiftfva  43005