![]() |
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. (Contributed by NM, 30-Oct-2003.) |
Ref | Expression |
---|---|
pwexg | ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 4425 | . . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
2 | 1 | eleq1d 2850 | . 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
3 | vpwex 5131 | . 2 ⊢ 𝒫 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3486 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 Vcvv 3415 𝒫 cpw 4422 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5060 ax-pow 5119 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-v 3417 df-in 3836 df-ss 3843 df-pw 4424 |
This theorem is referenced by: pwexd 5133 pwex 5134 abssexg 5135 snexALT 5136 pwel 5201 xpexg 7290 uniexr 7302 pwexb 7305 fabexg 7454 pw2eng 8419 2pwne 8469 disjen 8470 domss2 8472 ssenen 8487 fineqvlem 8527 tskwe 9173 ween 9255 acni 9265 acnnum 9272 infpwfien 9282 pwdju1 9414 ackbij1b 9459 fictb 9465 fin2i 9515 isfin2-2 9539 ssfin3ds 9550 fin23lem32 9564 fin23lem39 9570 fin23lem41 9572 isfin1-3 9606 fin1a2lem12 9631 canth3 9781 ondomon 9783 canthnum 9869 canthwe 9871 gchxpidm 9889 hashbcval 16194 restid2 16560 prdsplusg 16587 prdsvsca 16589 ismre 16719 isacs1i 16786 sscpwex 16943 fpwipodrs 17632 acsdrscl 17638 opsrval 19968 toponsspwpw 21234 tgdom 21290 distop 21307 fctop 21316 cctop 21318 ppttop 21319 epttop 21321 cldval 21335 ntrfval 21336 clsfval 21337 neifval 21411 neif 21412 neival 21414 neiptoptop 21443 lpfval 21450 restfpw 21491 islocfin 21829 dissnref 21840 kgenval 21847 dfac14lem 21929 qtopval 22007 isfbas 22141 fbssfi 22149 fsubbas 22179 fgval 22182 filssufil 22224 hauspwpwf1 22299 hauspwpwdom 22300 flimfnfcls 22340 tsmsfbas 22439 eltsms 22444 ustval 22514 utopval 22544 cusgrexilem1 26924 indv 30921 sigaex 31019 sigaval 31020 pwsiga 31040 pwldsys 31067 ldgenpisyslem1 31073 omsval 31202 carsgval 31212 coinflipspace 31390 iscvm 32097 cvmsval 32104 madeval 32816 altxpexg 32966 hfpw 33173 fnemeet2 33242 fnejoin1 33243 bj-restpw 33899 bj-discrmoore 33920 elrfi 38692 elrfirn 38693 kelac2 39067 enmappwid 39715 rfovd 39716 fsovrfovd 39724 dssmapfv2d 39733 clsk3nimkb 39759 clsneif1o 39823 clsneicnv 39824 clsneikex 39825 clsneinex 39826 neicvgmex 39836 neicvgel1 39838 pwsal 42037 prproropen 43044 |
Copyright terms: Public domain | W3C validator |