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 5216 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | mpg 1798 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3496 ⦋csb 3885 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-nul 5212 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-nul 4294 |
This theorem is referenced by: iunopeqop 5413 dfmpo 7799 cantnfdm 9129 cantnff 9139 bpolylem 15404 ruclem1 15586 pcmpt 16230 cidffn 16951 issubc 17107 natffn 17221 fnxpc 17428 evlfcl 17474 odf 18667 selvval 20333 itgfsum 24429 itgparts 24646 vmaf 25698 ttgval 26663 abfmpel 30402 msrf 32791 rdgssun 34661 finxpreclem2 34673 poimirlem17 34911 poimirlem23 34917 poimirlem24 34918 unirep 34990 cdlemk40 38055 aomclem6 39666 rnghmfn 44168 rngchomrnghmresALTV 44274 |
Copyright terms: Public domain | W3C validator |