![]() |
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 4612 | . . 3 ⊢ (𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴) | |
2 | 1 | eleq1d 2814 | . 2 ⊢ (𝑥 = 𝐴 → (𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
3 | vpwex 5371 | . 2 ⊢ 𝒫 𝑥 ∈ V | |
4 | 2, 3 | vtoclg 3539 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 Vcvv 3470 𝒫 cpw 4598 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5293 ax-pow 5359 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3472 df-in 3952 df-ss 3962 df-pw 4600 |
This theorem is referenced by: pwexd 5373 pwex 5374 pwel 5375 abssexg 5376 snexALT 5377 xpexg 7746 uniexr 7759 pwexb 7762 fabexg 7936 pw2eng 9096 2pwne 9151 disjen 9152 domss2 9154 ssenen 9169 fineqvlem 9280 tskwe 9967 ween 10052 acni 10062 acnnum 10069 infpwfien 10079 pwdju1 10207 ackbij1b 10256 fictb 10262 fin2i 10312 isfin2-2 10336 ssfin3ds 10347 fin23lem32 10361 fin23lem39 10367 fin23lem41 10369 isfin1-3 10403 fin1a2lem12 10428 canth3 10578 ondomon 10580 canthnum 10666 canthwe 10668 gchxpidm 10686 hashbcval 16964 restid2 17405 prdsplusg 17433 prdsvsca 17435 ismre 17563 isacs1i 17630 sscpwex 17791 fpwipodrs 18525 acsdrscl 18531 opsrval 21977 toponsspwpw 22817 tgdom 22874 distop 22891 fctop 22900 cctop 22902 ppttop 22903 epttop 22905 cldval 22920 ntrfval 22921 clsfval 22922 neifval 22996 neif 22997 neival 22999 neiptoptop 23028 lpfval 23035 restfpw 23076 islocfin 23414 dissnref 23425 kgenval 23432 dfac14lem 23514 qtopval 23592 isfbas 23726 fbssfi 23734 fsubbas 23764 fgval 23767 filssufil 23809 hauspwpwf1 23884 hauspwpwdom 23885 flimfnfcls 23925 tsmsfbas 24025 eltsms 24030 ustval 24100 utopval 24130 madeval 27772 cusgrexilem1 29245 pwrssmgc 32721 indv 33625 sigaex 33723 sigaval 33724 pwsiga 33743 pwldsys 33770 ldgenpisyslem1 33776 omsval 33907 carsgval 33917 coinflipspace 34094 iscvm 34863 cvmsval 34870 ex-sategoelel 35025 altxpexg 35568 hfpw 35775 fnemeet2 35845 fnejoin1 35846 bj-restpw 36565 elrfi 42108 elrfirn 42109 kelac2 42483 enmappwid 43424 rfovd 43425 fsovrfovd 43433 dssmapfv2d 43442 clsk3nimkb 43464 clsneif1o 43528 clsneicnv 43529 clsneikex 43530 clsneinex 43531 neicvgmex 43541 neicvgel1 43543 pwsal 45697 prproropen 46842 |
Copyright terms: Public domain | W3C validator |