![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pwexg | Structured version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 3961 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq1d 2520 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3071 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | pwex 4573 |
. 2
![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 3126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4511 ax-pow 4568 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-v 3070 df-in 3433 df-ss 3440 df-pw 3960 |
This theorem is referenced by: abssexg 4575 snexALT 4576 pwel 4642 uniexb 6486 xpexg 6607 fabexg 6633 undefval 6895 mapex 7320 pmvalg 7325 pw2eng 7517 fopwdom 7519 pwdom 7563 2pwne 7567 disjen 7568 domss2 7570 ssenen 7585 fineqvlem 7628 fival 7763 fipwuni 7777 hartogslem2 7858 wdompwdom 7894 harwdom 7906 tskwe 8221 ween 8306 acni 8316 acnnum 8323 infpwfien 8333 pwcda1 8464 ackbij1b 8509 fictb 8515 fin2i 8565 isfin2-2 8589 ssfin3ds 8600 fin23lem32 8614 fin23lem39 8620 fin23lem41 8622 isfin1-3 8656 fin1a2lem12 8681 canth3 8826 ondomon 8828 canthnum 8917 canthwe 8919 canthp1lem2 8921 gchxpidm 8937 gchpwdom 8938 gchhar 8947 wrdexg 12346 hashbcval 14165 restid2 14471 prdsplusg 14498 prdsmulr 14499 prdsvsca 14500 ismre 14630 isacs1i 14697 sscpwex 14830 fpwipodrs 15436 acsdrscl 15442 sylow2a 16222 opsrval 17663 istps3OLD 18643 tgdom 18699 distop 18716 fctop 18724 cctop 18726 ppttop 18727 epttop 18729 cldval 18743 ntrfval 18744 clsfval 18745 mretopd 18812 neifval 18819 neif 18820 neival 18822 neiptoptop 18851 lpfval 18858 restfpw 18899 ordtbaslem 18908 kgenval 19224 dfac14lem 19306 qtopval 19384 isfbas 19518 fbssfi 19526 fsubbas 19556 fgval 19559 filssufil 19601 hauspwpwf1 19676 hauspwpwdom 19677 flimfnfcls 19717 ptcmplem1 19740 tsmsfbas 19814 eltsms 19819 ustval 19893 isust 19894 utopval 19923 blfvalps 20074 cusgraexilem1 23509 issubgo 23925 indv 26603 sigaex 26686 sigaval 26687 pwsiga 26707 omsval 26842 omsfval 26843 coinflipspace 26997 iscvm 27282 cvmsval 27289 altxpexg 28143 hfpw 28357 islocfin 28706 neibastop2lem 28719 fnemeet2 28726 fnejoin1 28727 elrfi 29168 elrfirn 29169 kelac2 29556 |
Copyright terms: Public domain | W3C validator |