Theorem csbid 3868

Description: Analogue of sbid 2293 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 3856	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3764	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2832	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2902	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2792	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1563   ∈ wcel 2145  {cab 2743  [wsbc 3747  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sbc 3748  df-csb 3856

This theorem is referenced by:  csbeq1a  3869  fvmpt2f  6980  fvmpt2i  6990  fvmpocurryd  8255  fsumsplitf  15783  gsummoncoe1  22429  gsumply1eq  22430  disji2f  32832  disjif2  32836  disjabrex  32837  disjabrexf  32838  gsummpt2co  33281  measiuns  34524  fphpd  43405  disjrnmpt2  45764  climinf2mpt  46286  climinfmpt  46287  dvmptmulf  46509  sge0f1o  46954