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 5175 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | mpg 1804 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2113 Vcvv 3397 ⦋csb 3788 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-nul 5171 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-nul 4210 |
This theorem is referenced by: iunopeqop 5375 dfmpo 7816 cantnfdm 9193 cantnff 9203 bpolylem 15487 ruclem1 15669 pcmpt 16321 cidffn 17045 issubc 17203 natffn 17317 fnxpc 17535 evlfcl 17581 odf 18776 selvval 20925 itgfsum 24571 itgparts 24791 vmaf 25848 ttgval 26813 abfmpel 30559 msrf 33067 rdgssun 35161 finxpreclem2 35173 poimirlem17 35406 poimirlem23 35412 poimirlem24 35413 unirep 35483 cdlemk40 38543 aomclem6 40440 rnghmfn 44966 rngchomrnghmresALTV 45072 |
Copyright terms: Public domain | W3C validator |