Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version |
Description: Analogue of sbid 2257 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3886 | . 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} | |
2 | sbcid 3791 | . . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
3 | 2 | abbii 2888 | . 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴} |
4 | abid2 2959 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴 | |
5 | 1, 3, 4 | 3eqtri 2850 | 1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∈ wcel 2114 {cab 2801 [wsbc 3774 ⦋csb 3885 |
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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-12 2177 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-tru 1540 df-ex 1781 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-sbc 3775 df-csb 3886 |
This theorem is referenced by: csbeq1a 3899 fvmpt2f 6771 fvmpt2i 6780 fvmpocurryd 7939 fsumsplitf 15100 gsummoncoe1 20474 gsumply1eq 20475 disji2f 30329 disjif2 30333 disjabrex 30334 disjabrexf 30335 gsummpt2co 30688 measiuns 31478 fphpd 39420 disjrnmpt2 41456 climinf2mpt 42002 climinfmpt 42003 dvmptmulf 42229 sge0f1o 42671 |
Copyright terms: Public domain | W3C validator |