|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version | ||
| Description: Analogue of sbid 2254 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) | 
| Ref | Expression | 
|---|---|
| csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-csb 3899 | . 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} | |
| 2 | sbcid 3804 | . . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
| 3 | 2 | abbii 2808 | . 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴} | 
| 4 | abid2 2878 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴 | |
| 5 | 1, 3, 4 | 3eqtri 2768 | 1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: = wceq 1539 ∈ wcel 2107 {cab 2713 [wsbc 3787 ⦋csb 3898 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-12 2176 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-sbc 3788 df-csb 3899 | 
| This theorem is referenced by: csbeq1a 3912 fvmpt2f 7016 fvmpt2i 7025 fvmpocurryd 8297 fsumsplitf 15779 gsummoncoe1 22313 gsumply1eq 22314 disji2f 32591 disjif2 32595 disjabrex 32596 disjabrexf 32597 gsummpt2co 33052 measiuns 34219 fphpd 42832 disjrnmpt2 45198 climinf2mpt 45734 climinfmpt 45735 dvmptmulf 45957 sge0f1o 46402 | 
| Copyright terms: Public domain | W3C validator |