![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pwex | Structured version Unicode version |
Description: Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
zfpowcl.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pwex |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfpowcl.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | pweq 3970 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eleq1d 2523 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-pw 3969 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | axpow2 4579 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | bm1.3ii 4523 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | abeq2 2578 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | exbii 1635 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 6, 8 | mpbir 209 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | issetri 3083 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 4, 10 | eqeltri 2538 |
. 2
![]() ![]() ![]() ![]() ![]() |
12 | 1, 3, 11 | vtocl 3128 |
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 1955 ax-ext 2432 ax-sep 4520 ax-pow 4577 |
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 2440 df-cleq 2446 df-clel 2449 df-v 3078 df-in 3442 df-ss 3449 df-pw 3969 |
This theorem is referenced by: pwexg 4583 p0ex 4586 pp0ex 4588 ord3ex 4589 abexssex 6668 fnpm 7331 canth2 7573 dffi3 7791 inf3lem7 7950 r1sucg 8086 r1pwOLD 8163 rankuni 8180 rankc2 8188 rankxpu 8193 rankmapu 8195 rankxplim 8196 r0weon 8289 aceq3lem 8400 dfac5lem4 8406 dfac2a 8409 dfac2 8410 dfac8 8414 dfac13 8421 ackbij1lem5 8503 ackbij1lem8 8506 ackbij2lem2 8519 ackbij2lem3 8520 fin23lem17 8617 domtriomlem 8721 dominf 8724 axdc2lem 8727 axdc3lem 8729 numthcor 8773 axdclem2 8799 alephsucpw 8844 dominfac 8847 canthp1lem1 8929 gchac 8958 intwun 9012 wunex2 9015 eltsk2g 9028 inttsk 9051 tskcard 9058 intgru 9091 gruina 9095 axgroth6 9105 npex 9265 axcnex 9424 pnfxr 11202 mnfxr 11204 ixxex 11421 prdsval 14511 prdsds 14520 prdshom 14523 ismre 14646 fnmre 14647 fnmrc 14663 mrcfval 14664 mrisval 14686 mreacs 14714 wunfunc 14927 catcfuccl 15095 catcxpccl 15135 lubfval 15266 glbfval 15279 isacs5lem 15457 issubm 15593 issubg 15799 cntzfval 15956 pmtrfval 16074 sylow1lem2 16218 lsmfval 16257 pj1fval 16311 issubrg 16987 lssset 17137 lspfval 17176 islbs 17279 lbsext 17366 lbsexg 17367 sraval 17379 aspval 17521 ocvfval 18215 cssval 18231 isobs 18269 islinds 18362 istopon 18661 tgdom 18714 fncld 18757 leordtval2 18947 cnpfval 18969 iscnp2 18974 kgenf 19245 xkoopn 19293 xkouni 19303 dfac14 19322 xkoccn 19323 prdstopn 19332 xkoco1cn 19361 xkoco2cn 19362 xkococn 19364 xkoinjcn 19391 isfbas 19533 uzrest 19601 acufl 19621 alexsubALTlem2 19751 tsmsval2 19831 ustfn 19907 ustn0 19926 ishtpy 20675 vitali 21225 sspval 24272 shex 24765 hsupval 24888 fpwrelmap 26183 fpwrelmapffs 26184 isrnsigaOLD 26699 dmvlsiga 26716 eulerpartlem1 26893 eulerpartgbij 26898 eulerpartlemmf 26901 coinflippv 27009 ballotlemoex 27011 kur14lem9 27245 heibor1lem 28855 heibor 28867 idlval 28960 mzpclval 29208 eldiophb 29242 rpnnen3 29528 dfac11 29562 rgspnval 29672 lincop 31060 bj-snglex 32783 psubspset 33711 paddfval 33764 pclfvalN 33856 polfvalN 33871 psubclsetN 33903 docafvalN 35090 djafvalN 35102 dicval 35144 dochfval 35318 djhfval 35365 islpolN 35451 |
Copyright terms: Public domain | W3C validator |