![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sselpwd | Structured version Visualization version GIF version |
Description: Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.) |
Ref | Expression |
---|---|
sselpwd.1 | ⊢ (𝜑 → 𝐵 ∈ 𝑉) |
sselpwd.2 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
Ref | Expression |
---|---|
sselpwd | ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sselpwd.1 | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑉) | |
2 | sselpwd.2 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
3 | 1, 2 | ssexd 5281 | . 2 ⊢ (𝜑 → 𝐴 ∈ V) |
4 | 3, 2 | elpwd 4566 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2106 Vcvv 3445 ⊆ wss 3910 𝒫 cpw 4560 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5256 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3408 df-v 3447 df-in 3917 df-ss 3927 df-pw 4562 |
This theorem is referenced by: knatar 7301 marypha1 9369 fin1a2lem7 10341 canthp1lem2 10588 wunss 10647 ramub1lem1 16897 mreexd 17521 mreexexlemd 17523 mreexexlem4d 17526 opsrval 21445 selvfval 21525 cncls 22623 fbasrn 23233 rnelfmlem 23301 ustssel 23555 pwrssmgc 31804 crefi 32368 ldsysgenld 32699 ldgenpisyslem1 32702 bj-ismoored 35568 bj-imdirval2 35644 bj-iminvval2 35655 sticksstones2 40545 rfovcnvf1od 42257 fsovrfovd 42262 fsovfd 42265 fsovcnvlem 42266 ntrclsrcomplex 42288 clsk3nimkb 42293 clsk1indlem4 42297 clsk1indlem1 42298 ntrclsiso 42320 ntrclskb 42322 ntrclsk3 42323 ntrclsk13 42324 ntrneircomplex 42327 ntrneik3 42349 ntrneix3 42350 ntrneik13 42351 ntrneix13 42352 clsneircomplex 42356 clsneiel1 42361 neicvgrcomplex 42366 neicvgel1 42372 mnussd 42524 mnuprssd 42530 mnuop3d 42532 wessf1ornlem 43378 ovolsplit 44200 saliunclf 44534 iscnrm3rlem3 46946 |
Copyright terms: Public domain | W3C validator |