![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbex | Structured version Visualization version GIF version |
Description: The existence of proper substitution into a class. (Contributed by NM, 7-Aug-2007.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Revised by NM, 17-Aug-2018.) |
Ref | Expression |
---|---|
csbex.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
csbex | ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbexg 5311 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | mpg 1800 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 ⦋csb 3894 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-nul 4324 |
This theorem is referenced by: iunopeqop 5522 dfmpo 8088 cantnfdm 9659 cantnff 9669 bpolylem 15992 ruclem1 16174 pcmpt 16825 cidffn 17622 issubc 17785 natffn 17900 fnxpc 18128 evlfcl 18175 odf 19405 selvval 21681 itgfsum 25344 itgparts 25564 vmaf 26623 mulsval 27565 precsexlem3 27655 ttgval 28126 ttgvalOLD 28127 abfmpel 31880 msrf 34533 rdgssun 36259 finxpreclem2 36271 poimirlem17 36505 poimirlem23 36511 poimirlem24 36512 unirep 36582 cdlemk40 39788 aomclem6 41801 rnghmfn 46688 rngchomrnghmresALTV 46894 |
Copyright terms: Public domain | W3C validator |