| 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 5324 | . 2 ⊢ (𝜑 → 𝐴 ∈ V) |
| 4 | 3, 2 | elpwd 4606 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 |
| 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-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: knatar 7377 marypha1 9474 fin1a2lem7 10446 canthp1lem2 10693 wunss 10752 ramub1lem1 17064 mreexd 17685 mreexexlemd 17687 mreexexlem4d 17690 opsrval 22064 selvfval 22138 cncls 23282 fbasrn 23892 rnelfmlem 23960 ustssel 24214 pwrssmgc 32990 exsslsb 33647 crefi 33846 ldsysgenld 34161 ldgenpisyslem1 34164 bj-ismoored 37108 bj-imdirval2 37184 bj-iminvval2 37195 sticksstones2 42148 rfovcnvf1od 44017 fsovrfovd 44022 fsovfd 44025 fsovcnvlem 44026 ntrclsrcomplex 44048 clsk3nimkb 44053 clsk1indlem4 44057 clsk1indlem1 44058 ntrclsiso 44080 ntrclskb 44082 ntrclsk3 44083 ntrclsk13 44084 ntrneircomplex 44087 ntrneik3 44109 ntrneix3 44110 ntrneik13 44111 ntrneix13 44112 clsneircomplex 44116 clsneiel1 44121 neicvgrcomplex 44126 neicvgel1 44132 mnussd 44282 mnuprssd 44288 mnuop3d 44290 wessf1ornlem 45190 dvnprodlem1 45961 ovolsplit 46003 saliunclf 46337 sge0f1o 46397 isisubgr 47848 iscnrm3rlem3 48839 |
| Copyright terms: Public domain | W3C validator |