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 5270 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 𝒫 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2108 Vcvv 3493 𝒫 cpw 4537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 ax-pow 5257 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-v 3495 df-in 3941 df-ss 3950 df-pw 4539 |
This theorem is referenced by: undefval 7934 mapex 8404 pmvalg 8409 fopwdom 8617 pwdom 8661 fineqvlem 8724 fival 8868 fipwuni 8882 hartogslem2 8999 wdompwdom 9034 harwdom 9046 canthwe 10065 canthp1lem2 10067 gchdjuidm 10082 gchpwdom 10084 gchhar 10093 wrdexgOLD 13864 prdsmulr 16724 sylow2a 18736 selvffval 20321 toponsspwpw 21522 mretopd 21692 ordtbaslem 21788 ptcmplem1 22652 isust 22804 blfvalps 22985 carsgval 31554 neibastop2lem 33701 bj-imdirval 34464 bj-imdirval2 34465 rfovcnvf1od 40341 fsovfd 40349 fsovcnvlem 40350 dssmapnvod 40357 dssmapf1od 40358 ntrneif1o 40416 ntrneicnv 40419 ntrneiel 40422 clsneiel1 40449 neicvgf1o 40455 neicvgnvo 40456 neicvgel1 40460 ntrelmap 40466 clselmap 40468 salexct 42608 psmeasurelem 42743 caragenval 42766 omeunile 42778 0ome 42802 isomennd 42804 afv2ex 43404 |
Copyright terms: Public domain | W3C validator |