Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pwexg | Structured version Visualization version GIF version |
Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) |
Ref | Expression |
---|---|
pwexg | ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 4111 | . . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
2 | 1 | eleq1d 2672 | . 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
3 | vpwex 4775 | . 2 ⊢ 𝒫 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3239 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∈ wcel 1977 Vcvv 3173 𝒫 cpw 4108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-pow 4769 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 |
This theorem is referenced by: abssexg 4777 snexALT 4778 pwel 4847 xpexg 6858 uniexb 6866 fabexg 7015 undefval 7289 mapex 7750 pmvalg 7755 pw2eng 7951 fopwdom 7953 pwdom 7997 2pwne 8001 disjen 8002 domss2 8004 ssenen 8019 fineqvlem 8059 fival 8201 fipwuni 8215 hartogslem2 8331 wdompwdom 8366 harwdom 8378 tskwe 8659 ween 8741 acni 8751 acnnum 8758 infpwfien 8768 pwcda1 8899 ackbij1b 8944 fictb 8950 fin2i 9000 isfin2-2 9024 ssfin3ds 9035 fin23lem32 9049 fin23lem39 9055 fin23lem41 9057 isfin1-3 9091 fin1a2lem12 9116 canth3 9262 ondomon 9264 canthnum 9350 canthwe 9352 canthp1lem2 9354 gchxpidm 9370 gchpwdom 9371 gchhar 9380 wrdexg 13170 hashbcval 15544 restid2 15914 prdsplusg 15941 prdsmulr 15942 prdsvsca 15943 ismre 16073 isacs1i 16141 sscpwex 16298 fpwipodrs 16987 acsdrscl 16993 sylow2a 17857 opsrval 19295 tgdom 20593 distop 20610 fctop 20618 cctop 20620 ppttop 20621 epttop 20623 cldval 20637 ntrfval 20638 clsfval 20639 mretopd 20706 neifval 20713 neif 20714 neival 20716 neiptoptop 20745 lpfval 20752 restfpw 20793 ordtbaslem 20802 islocfin 21130 dissnref 21141 kgenval 21148 dfac14lem 21230 qtopval 21308 isfbas 21443 fbssfi 21451 fsubbas 21481 fgval 21484 filssufil 21526 hauspwpwf1 21601 hauspwpwdom 21602 flimfnfcls 21642 ptcmplem1 21666 tsmsfbas 21741 eltsms 21746 ustval 21816 isust 21817 utopval 21846 blfvalps 21998 cusgraexilem1 25995 indv 29402 sigaex 29499 sigaval 29500 pwsiga 29520 pwldsys 29547 ldgenpisyslem1 29553 omsval 29682 carsgval 29692 coinflipspace 29869 iscvm 30495 cvmsval 30502 altxpexg 31255 hfpw 31462 neibastop2lem 31525 fnemeet2 31532 fnejoin1 31533 bj-restpw 32226 bj-toponss 32241 elrfi 36275 elrfirn 36276 kelac2 36653 enmappwid 37314 rfovd 37315 rfovcnvf1od 37318 fsovrfovd 37323 fsovfd 37326 fsovcnvlem 37327 dssmapfv2d 37332 dssmapnvod 37334 dssmapf1od 37335 clsk3nimkb 37358 ntrneif1o 37393 ntrneicnv 37396 ntrneiel 37399 clsneif1o 37422 clsneicnv 37423 clsneikex 37424 clsneinex 37425 clsneiel1 37426 neicvgf1o 37432 neicvgnvo 37433 neicvgmex 37435 neicvgel1 37437 ntrelmap 37443 clselmap 37445 pwexd 38311 pwsal 39211 salexct 39228 psmeasurelem 39363 caragenval 39383 omeunile 39395 0ome 39419 isomennd 39421 usgrexi 40661 |
Copyright terms: Public domain | W3C validator |