Theorem csbid 3907

Description: Analogue of sbid 2248 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 3895	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3795	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2803	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2872	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2765	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1542   ∈ wcel 2107  {cab 2710  [wsbc 3778  ⦋csb 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sbc 3779  df-csb 3895

This theorem is referenced by:  csbeq1a  3908  fvmpt2f  7000  fvmpt2i  7009  fvmpocurryd  8256  fsumsplitf  15688  gsummoncoe1  21828  gsumply1eq  21829  disji2f  31808  disjif2  31812  disjabrex  31813  disjabrexf  31814  gsummpt2co  32200  measiuns  33215  fphpd  41554  disjrnmpt2  43886  climinf2mpt  44430  climinfmpt  44431  dvmptmulf  44653  sge0f1o  45098