Theorem csbid 3859

Description: Analogue of sbid 2260 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 3847	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3754	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2800	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2870	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2760	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  {cab 2711  [wsbc 3737  ⦋csb 3846

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 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sbc 3738  df-csb 3847

This theorem is referenced by:  csbeq1a  3860  fvmpt2f  6936  fvmpt2i  6945  fvmpocurryd  8207  fsumsplitf  15651  gsummoncoe1  22224  gsumply1eq  22225  disji2f  32559  disjif2  32563  disjabrex  32564  disjabrexf  32565  gsummpt2co  33035  measiuns  34251  fphpd  42933  disjrnmpt2  45309  climinf2mpt  45836  climinfmpt  45837  dvmptmulf  46059  sge0f1o  46504