Theorem csbid 3823

Description: Analogue of sbid 2220 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 3812	. 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴}
2		sbcid 3723	. . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)
3	2	abbii 2861	. 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴}
4		abid2 2926	. 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴
5	1, 3, 4	3eqtri 2823	1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴

Syntax hints:   = wceq 1522   ∈ wcel 2081  {cab 2775  [wsbc 3706  ⦋csb 3811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1525  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-sbc 3707  df-csb 3812

This theorem is referenced by:  csbeq1a  3824  fvmpt2f  6636  fvmpt2i  6644  fvmpocurryd  7788  fsumsplitf  14931  gsummoncoe1  20155  gsumply1eq  20156  disji2f  30017  disjif2  30021  disjabrex  30022  disjabrexf  30023  gsummpt2co  30495  measiuns  31093  fphpd  38898  disjrnmpt2  40989  climinf2mpt  41537  climinfmpt  41538  dvmptmulf  41763  sge0f1o  42206