![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwex | Structured version Visualization 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 3956 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eleq1d 2515 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-pw 3955 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | axpow2 4586 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 5 | bm1.3ii 4531 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | abeq2 2562 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 7 | exbii 1720 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 6, 8 | mpbir 213 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | issetri 3054 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | 4, 10 | eqeltri 2527 |
. 2
![]() ![]() ![]() ![]() ![]() |
12 | 1, 3, 11 | vtocl 3102 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-pow 4584 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-v 3049 df-in 3413 df-ss 3420 df-pw 3955 |
This theorem is referenced by: pwexg 4590 p0ex 4593 pp0ex 4595 ord3ex 4596 abexssex 6780 fnpm 7485 canth2 7730 dffi3 7950 inf3lem7 8144 r1sucg 8245 r1pwALT 8322 rankuni 8339 rankc2 8347 rankxpu 8352 rankmapu 8354 rankxplim 8355 r0weon 8448 aceq3lem 8556 dfac5lem4 8562 dfac2a 8565 dfac2 8566 dfac8 8570 dfac13 8577 ackbij1lem5 8659 ackbij1lem8 8662 ackbij2lem2 8675 ackbij2lem3 8676 fin23lem17 8773 domtriomlem 8877 dominf 8880 axdc2lem 8883 axdc3lem 8885 numthcor 8929 axdclem2 8955 alephsucpw 9000 dominfac 9003 canthp1lem1 9082 gchac 9111 intwun 9165 wunex2 9168 eltsk2g 9181 inttsk 9204 tskcard 9211 intgru 9244 gruina 9248 axgroth6 9258 npex 9416 axcnex 9576 pnfxr 11419 mnfxr 11421 ixxex 11653 prdsval 15365 prdsds 15374 prdshom 15377 ismre 15508 fnmre 15509 fnmrc 15525 mrcfval 15526 mrisval 15548 mreacs 15576 wunfunc 15816 catcfuccl 16016 catcxpccl 16104 lubfval 16236 glbfval 16249 isacs5lem 16427 issubm 16606 issubg 16829 cntzfval 16986 pmtrfval 17103 sylow1lem2 17263 lsmfval 17302 pj1fval 17356 issubrg 18020 lssset 18169 lspfval 18208 islbs 18311 lbsext 18398 lbsexg 18399 sraval 18411 aspval 18564 ocvfval 19241 cssval 19257 isobs 19295 islinds 19379 istopon 19952 tgdom 20006 fncld 20049 leordtval2 20240 cnpfval 20262 iscnp2 20267 kgenf 20568 xkoopn 20616 xkouni 20626 dfac14 20645 xkoccn 20646 prdstopn 20655 xkoco1cn 20684 xkoco2cn 20685 xkococn 20687 xkoinjcn 20714 isfbas 20856 uzrest 20924 acufl 20944 alexsubALTlem2 21075 tsmsval2 21156 ustfn 21228 ustn0 21247 ishtpy 22015 vitali 22583 sspval 26374 shex 26877 hsupval 26999 fpwrelmap 28330 fpwrelmapffs 28331 isrnsigaOLD 28946 dmvlsiga 28963 eulerpartlem1 29212 eulerpartgbij 29217 eulerpartlemmf 29220 coinflippv 29328 ballotlemoex 29330 kur14lem9 29949 mpstval 30185 mclsrcl 30211 mclsval 30213 bj-snglex 31579 heibor1lem 32153 heibor 32165 idlval 32258 psubspset 33321 paddfval 33374 pclfvalN 33466 polfvalN 33481 psubclsetN 33513 docafvalN 34702 djafvalN 34714 dicval 34756 dochfval 34930 djhfval 34977 islpolN 35063 mzpclval 35579 eldiophb 35611 rpnnen3 35899 dfac11 35932 rgspnval 36046 pwinfi 36180 ovnval 38372 usgsizedg 39811 usgsizedgALT 39812 usgsizedgALT2 39813 issubmgm 39893 lincop 40305 |
Copyright terms: Public domain | W3C validator |