Theorem csbid 3863

Description: Analogue of sbid 2292 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 3851	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3759	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2829	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2899	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2789	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2740  [wsbc 3742  ⦋csb 3850

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 2215  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743  df-csb 3851

This theorem is used by:  csbeq1a  3864  fvmpt2f  6991  fvmpt2i  7001  fvmpocurryd  8272  fsumsplitf  15830  gsummoncoe1  22537  gsumply1eq  22538  disji2f  33052  disjif2  33056  disjabrex  33057  disjabrexf  33058  gsummpt2co  33490  measiuns  34730  fphpd  43659  disjrnmpt2  46022  climinf2mpt  46544  climinfmpt  46545  dvmptmulf  46767  sge0f1o  47212