Theorem csbid 3862

Description: Analogue of sbid 2262 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbid	⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Proof of Theorem csbid

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-csb 3850	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3757	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2803	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2873	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2763	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2714  [wsbc 3740  ⦋csb 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3741  df-csb 3850

This theorem is referenced by:  csbeq1a  3863  fvmpt2f  6942  fvmpt2i  6951  fvmpocurryd  8213  fsumsplitf  15665  gsummoncoe1  22252  gsumply1eq  22253  disji2f  32652  disjif2  32656  disjabrex  32657  disjabrexf  32658  gsummpt2co  33131  measiuns  34374  fphpd  43054  disjrnmpt2  45428  climinf2mpt  45954  climinfmpt  45955  dvmptmulf  46177  sge0f1o  46622