Theorem csbid 3860

Description: Analogue of sbid 2291 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 3848	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3756	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2828	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2898	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2788	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2739  [wsbc 3739  ⦋csb 3847

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740  df-csb 3848

This theorem is used by:  csbeq1a  3861  fvmpt2f  6986  fvmpt2i  6996  fvmpocurryd  8272  fsumsplitf  15888  gsummoncoe1  22606  gsumply1eq  22607  disji2f  33153  disjif2  33157  disjabrex  33158  disjabrexf  33159  gsummpt2co  33591  measiuns  34832  fphpd  43776  disjrnmpt2  46146  climinf2mpt  46668  climinfmpt  46669  dvmptmulf  46891  sge0f1o  47336