![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version |
Description: Analogue of sbid 2220 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
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 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |