![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version |
Description: Analogue of sbid 2243 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3892 | . 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} | |
2 | sbcid 3792 | . . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
3 | 2 | abbii 2796 | . 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴} |
4 | abid2 2864 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴 | |
5 | 1, 3, 4 | 3eqtri 2758 | 1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∈ wcel 2099 {cab 2703 [wsbc 3775 ⦋csb 3891 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-sbc 3776 df-csb 3892 |
This theorem is referenced by: csbeq1a 3905 fvmpt2f 7002 fvmpt2i 7011 fvmpocurryd 8278 fsumsplitf 15741 gsummoncoe1 22296 gsumply1eq 22297 disji2f 32497 disjif2 32501 disjabrex 32502 disjabrexf 32503 gsummpt2co 32920 measiuns 34063 fphpd 42510 disjrnmpt2 44831 climinf2mpt 45371 climinfmpt 45372 dvmptmulf 45594 sge0f1o 46039 |
Copyright terms: Public domain | W3C validator |