![]() |
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 4194 | . . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
2 | 1 | eleq1d 2715 | . 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
3 | vpwex 4879 | . 2 ⊢ 𝒫 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3297 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 Vcvv 3231 𝒫 cpw 4191 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-pow 4873 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-v 3233 df-in 3614 df-ss 3621 df-pw 4193 |
This theorem is referenced by: abssexg 4881 snexALT 4882 pwel 4950 xpexg 7002 uniexr 7014 pwexb 7017 fabexg 7164 undefval 7447 mapex 7905 pmvalg 7910 pw2eng 8107 fopwdom 8109 pwdom 8153 2pwne 8157 disjen 8158 domss2 8160 ssenen 8175 fineqvlem 8215 fival 8359 fipwuni 8373 hartogslem2 8489 wdompwdom 8524 harwdom 8536 tskwe 8814 ween 8896 acni 8906 acnnum 8913 infpwfien 8923 pwcda1 9054 ackbij1b 9099 fictb 9105 fin2i 9155 isfin2-2 9179 ssfin3ds 9190 fin23lem32 9204 fin23lem39 9210 fin23lem41 9212 isfin1-3 9246 fin1a2lem12 9271 canth3 9421 ondomon 9423 canthnum 9509 canthwe 9511 canthp1lem2 9513 gchxpidm 9529 gchpwdom 9530 gchhar 9539 wrdexg 13347 hashbcval 15753 restid2 16138 prdsplusg 16165 prdsmulr 16166 prdsvsca 16167 ismre 16297 isacs1i 16365 sscpwex 16522 fpwipodrs 17211 acsdrscl 17217 sylow2a 18080 opsrval 19522 toponsspwpw 20774 tgdom 20830 distop 20847 fctop 20856 cctop 20858 ppttop 20859 epttop 20861 cldval 20875 ntrfval 20876 clsfval 20877 mretopd 20944 neifval 20951 neif 20952 neival 20954 neiptoptop 20983 lpfval 20990 restfpw 21031 ordtbaslem 21040 islocfin 21368 dissnref 21379 kgenval 21386 dfac14lem 21468 qtopval 21546 isfbas 21680 fbssfi 21688 fsubbas 21718 fgval 21721 filssufil 21763 hauspwpwf1 21838 hauspwpwdom 21839 flimfnfcls 21879 ptcmplem1 21903 tsmsfbas 21978 eltsms 21983 ustval 22053 isust 22054 utopval 22083 blfvalps 22235 cusgrexilem1 26391 indv 30202 sigaex 30300 sigaval 30301 pwsiga 30321 pwldsys 30348 ldgenpisyslem1 30354 omsval 30483 carsgval 30493 coinflipspace 30670 iscvm 31367 cvmsval 31374 madeval 32060 altxpexg 32210 hfpw 32417 neibastop2lem 32480 fnemeet2 32487 fnejoin1 32488 bj-restpw 33170 bj-discrmoore 33191 elrfi 37574 elrfirn 37575 kelac2 37952 enmappwid 38611 rfovd 38612 rfovcnvf1od 38615 fsovrfovd 38620 fsovfd 38623 fsovcnvlem 38624 dssmapfv2d 38629 dssmapnvod 38631 dssmapf1od 38632 clsk3nimkb 38655 ntrneif1o 38690 ntrneicnv 38693 ntrneiel 38696 clsneif1o 38719 clsneicnv 38720 clsneikex 38721 clsneinex 38722 clsneiel1 38723 neicvgf1o 38729 neicvgnvo 38730 neicvgmex 38732 neicvgel1 38734 ntrelmap 38740 clselmap 38742 pwexd 39596 pwsal 40853 salexct 40870 psmeasurelem 41005 caragenval 41028 omeunile 41040 0ome 41064 isomennd 41066 |
Copyright terms: Public domain | W3C validator |