![]() |
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 5178 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | mpg 1799 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Vcvv 3441 ⦋csb 3828 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-nul 5174 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-nul 4244 |
This theorem is referenced by: iunopeqop 5376 dfmpo 7780 cantnfdm 9111 cantnff 9121 bpolylem 15394 ruclem1 15576 pcmpt 16218 cidffn 16941 issubc 17097 natffn 17211 fnxpc 17418 evlfcl 17464 odf 18657 selvval 20790 itgfsum 24430 itgparts 24650 vmaf 25704 ttgval 26669 abfmpel 30418 msrf 32902 rdgssun 34795 finxpreclem2 34807 poimirlem17 35074 poimirlem23 35080 poimirlem24 35081 unirep 35151 cdlemk40 38213 aomclem6 40003 rnghmfn 44514 rngchomrnghmresALTV 44620 |
Copyright terms: Public domain | W3C validator |