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 5234 | . 2 ⊢ (∀𝑥 𝐵 ∈ V → ⦋𝐴 / 𝑥⦌𝐵 ∈ V) | |
2 | csbex.1 | . 2 ⊢ 𝐵 ∈ V | |
3 | 1, 2 | mpg 1800 | 1 ⊢ ⦋𝐴 / 𝑥⦌𝐵 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3432 ⦋csb 3832 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-nul 5230 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-nul 4257 |
This theorem is referenced by: iunopeqop 5435 dfmpo 7942 cantnfdm 9422 cantnff 9432 bpolylem 15758 ruclem1 15940 pcmpt 16593 cidffn 17387 issubc 17550 natffn 17665 fnxpc 17893 evlfcl 17940 odf 19145 selvval 21328 itgfsum 24991 itgparts 25211 vmaf 26268 ttgval 27236 ttgvalOLD 27237 abfmpel 30992 msrf 33504 rdgssun 35549 finxpreclem2 35561 poimirlem17 35794 poimirlem23 35800 poimirlem24 35801 unirep 35871 cdlemk40 38931 aomclem6 40884 rnghmfn 45448 rngchomrnghmresALTV 45554 |
Copyright terms: Public domain | W3C validator |