| 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 5310 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
| 2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
| 3 | 1, 2 | mpg 1797 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ⦋csb 3899 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-nul 5306 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: iunopeqop 5526 dfmpo 8127 cantnfdm 9704 cantnff 9714 bpolylem 16084 ruclem1 16267 pcmpt 16930 cidffn 17721 issubc 17880 natffn 17997 fnxpc 18221 evlfcl 18267 odf 19555 rnghmfn 20439 selvval 22139 itgfsum 25862 itgparts 26088 vmaf 27162 mulsval 28135 precsexlem3 28233 ttgval 28883 ttgvalOLD 28884 abfmpel 32665 msrf 35547 rdgssun 37379 finxpreclem2 37391 poimirlem17 37644 poimirlem23 37650 poimirlem24 37651 unirep 37721 cdlemk40 40919 aomclem6 43071 rngchomrnghmresALTV 48195 fucofn2 49019 |
| Copyright terms: Public domain | W3C validator |