![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version |
Description: Analogue of sbid 2248 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3893 | . 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} | |
2 | sbcid 3793 | . . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
3 | 2 | abbii 2803 | . 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴} |
4 | abid2 2872 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴 | |
5 | 1, 3, 4 | 3eqtri 2765 | 1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∈ wcel 2107 {cab 2710 [wsbc 3776 ⦋csb 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-sbc 3777 df-csb 3893 |
This theorem is referenced by: csbeq1a 3906 fvmpt2f 6995 fvmpt2i 7004 fvmpocurryd 8251 fsumsplitf 15684 gsummoncoe1 21810 gsumply1eq 21811 disji2f 31786 disjif2 31790 disjabrex 31791 disjabrexf 31792 gsummpt2co 32178 measiuns 33153 fphpd 41487 disjrnmpt2 43819 climinf2mpt 44365 climinfmpt 44366 dvmptmulf 44588 sge0f1o 45033 |
Copyright terms: Public domain | W3C validator |