Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbid | Structured version Visualization version GIF version |
Description: Analogue of sbid 2100 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbid | ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb 3500 | . 2 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} | |
2 | sbcid 3419 | . . 3 ⊢ ([𝑥 / 𝑥]𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴) | |
3 | 2 | abbii 2726 | . 2 ⊢ {𝑦 ∣ [𝑥 / 𝑥]𝑦 ∈ 𝐴} = {𝑦 ∣ 𝑦 ∈ 𝐴} |
4 | abid2 2732 | . 2 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐴} = 𝐴 | |
5 | 1, 3, 4 | 3eqtri 2636 | 1 ⊢ ⦋𝑥 / 𝑥⦌𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∈ wcel 1977 {cab 2596 [wsbc 3402 ⦋csb 3499 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-sbc 3403 df-csb 3500 |
This theorem is referenced by: csbeq1a 3508 fvmpt2f 6192 fvmpt2i 6199 fvmpt2curryd 7284 gsummoncoe1 19495 gsumply1eq 19496 disji2f 28772 disjif2 28776 disjabrex 28777 disjabrexf 28778 gsummpt2co 29111 measiuns 29607 fphpd 36398 disjrnmpt2 38370 fsumsplitf 38634 dvmptmulf 38827 sge0f1o 39275 |
Copyright terms: Public domain | W3C validator |