| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > pwexd | Structured version Visualization version GIF version | ||
| Description: Deduction version of the power set axiom. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
| Ref | Expression |
|---|---|
| pwexd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| Ref | Expression |
|---|---|
| pwexd | ⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pwexd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉) | |
| 2 | pwexg 5378 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3480 𝒫 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 ax-pow 5365 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: fabexd 7959 undefval 8301 mapexOLD 8872 pmvalg 8877 fopwdom 9120 pwdom 9169 fineqvlem 9298 fival 9452 fipwuni 9466 hartogslem2 9583 wdompwdom 9618 harwdom 9631 canthwe 10691 canthp1lem2 10693 gchdjuidm 10708 gchpwdom 10710 gchhar 10719 prdsmulr 17504 selvffval 22137 toponsspwpw 22928 mretopd 23100 ordtbaslem 23196 ptcmplem1 24060 isust 24212 blfvalps 24393 carsgval 34305 neibastop2lem 36361 bj-imdirvallem 37181 bj-imdirval2lem 37183 rfovcnvf1od 44017 fsovfd 44025 fsovcnvlem 44026 dssmapnvod 44033 dssmapf1od 44034 ntrneif1o 44088 ntrneicnv 44091 ntrneiel 44094 clsneiel1 44121 neicvgf1o 44127 neicvgnvo 44128 neicvgel1 44132 ntrelmap 44138 clselmap 44140 salexct 46349 psmeasurelem 46485 caragenval 46508 omeunile 46520 0ome 46544 isomennd 46546 afv2ex 47226 gpgvtx 48002 gpgiedg 48003 |
| Copyright terms: Public domain | W3C validator |