Theorem csbid 3845

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 3833	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3733	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2808	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2882	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2770	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2106  {cab 2715  [wsbc 3716  ⦋csb 3832

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sbc 3717  df-csb 3833

This theorem is referenced by:  csbeq1a  3846  fvmpt2f  6876  fvmpt2i  6885  fvmpocurryd  8087  fsumsplitf  15454  gsummoncoe1  21475  gsumply1eq  21476  disji2f  30916  disjif2  30920  disjabrex  30921  disjabrexf  30922  gsummpt2co  31308  measiuns  32185  fphpd  40638  disjrnmpt2  42726  climinf2mpt  43255  climinfmpt  43256  dvmptmulf  43478  sge0f1o  43920