Theorem csbid 3905

Description: Analogue of sbid 2247 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 3893	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3793	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2802	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2871	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2764	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2106  {cab 2709  [wsbc 3776  ⦋csb 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sbc 3777  df-csb 3893

This theorem is referenced by:  csbeq1a  3906  fvmpt2f  6996  fvmpt2i  7005  fvmpocurryd  8252  fsumsplitf  15684  gsummoncoe1  21819  gsumply1eq  21820  disji2f  31795  disjif2  31799  disjabrex  31800  disjabrexf  31801  gsummpt2co  32187  measiuns  33203  fphpd  41539  disjrnmpt2  43871  climinf2mpt  44416  climinfmpt  44417  dvmptmulf  44639  sge0f1o  45084