Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pwex | Structured version Visualization version GIF 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 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
pwex | ⊢ 𝒫 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zfpowcl.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | pweq 4111 | . . 3 ⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴) | |
3 | 2 | eleq1d 2672 | . 2 ⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∈ V ↔ 𝒫 𝐴 ∈ V)) |
4 | df-pw 4110 | . . 3 ⊢ 𝒫 𝑧 = {𝑦 ∣ 𝑦 ⊆ 𝑧} | |
5 | axpow2 4771 | . . . . . 6 ⊢ ∃𝑥∀𝑦(𝑦 ⊆ 𝑧 → 𝑦 ∈ 𝑥) | |
6 | 5 | bm1.3ii 4712 | . . . . 5 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧) |
7 | abeq2 2719 | . . . . . 6 ⊢ (𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)) | |
8 | 7 | exbii 1764 | . . . . 5 ⊢ (∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ⊆ 𝑧)) |
9 | 6, 8 | mpbir 220 | . . . 4 ⊢ ∃𝑥 𝑥 = {𝑦 ∣ 𝑦 ⊆ 𝑧} |
10 | 9 | issetri 3183 | . . 3 ⊢ {𝑦 ∣ 𝑦 ⊆ 𝑧} ∈ V |
11 | 4, 10 | eqeltri 2684 | . 2 ⊢ 𝒫 𝑧 ∈ V |
12 | 1, 3, 11 | vtocl 3232 | 1 ⊢ 𝒫 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 Vcvv 3173 ⊆ wss 3540 𝒫 cpw 4108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-pow 4769 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 |
This theorem is referenced by: vpwex 4775 p0ex 4779 pp0ex 4781 ord3ex 4782 abexssex 7041 fnpm 7752 canth2 7998 dffi3 8220 r1sucg 8515 r1pwALT 8592 rankuni 8609 rankc2 8617 rankxpu 8622 rankmapu 8624 rankxplim 8625 r0weon 8718 aceq3lem 8826 dfac5lem4 8832 dfac2a 8835 dfac2 8836 ackbij2lem2 8945 ackbij2lem3 8946 fin23lem17 9043 domtriomlem 9147 axdc2lem 9153 axdc3lem 9155 axdclem2 9225 alephsucpw 9271 canthp1lem1 9353 gchac 9382 gruina 9519 npex 9687 axcnex 9847 pnfxr 9971 mnfxr 9975 ixxex 12057 prdsval 15938 prdsds 15947 prdshom 15950 ismre 16073 fnmre 16074 fnmrc 16090 mrcfval 16091 mrisval 16113 wunfunc 16382 catcfuccl 16582 catcxpccl 16670 lubfval 16801 glbfval 16814 issubm 17170 issubg 17417 cntzfval 17576 sylow1lem2 17837 lsmfval 17876 pj1fval 17930 issubrg 18603 lssset 18755 lspfval 18794 islbs 18897 lbsext 18984 lbsexg 18985 sraval 18997 aspval 19149 ocvfval 19829 cssval 19845 isobs 19883 islinds 19967 istopon 20540 fncld 20636 leordtval2 20826 cnpfval 20848 iscnp2 20853 kgenf 21154 xkoopn 21202 xkouni 21212 dfac14 21231 xkoccn 21232 prdstopn 21241 xkoco1cn 21270 xkoco2cn 21271 xkococn 21273 xkoinjcn 21300 isfbas 21443 uzrest 21511 acufl 21531 alexsubALTlem2 21662 tsmsval2 21743 ustfn 21815 ustn0 21834 ishtpy 22579 vitali 23188 sspval 26962 shex 27453 hsupval 27577 fpwrelmap 28896 fpwrelmapffs 28897 isrnsigaOLD 29502 dmvlsiga 29519 eulerpartlem1 29756 eulerpartgbij 29761 eulerpartlemmf 29764 coinflippv 29872 ballotlemoex 29874 kur14lem9 30450 mpstval 30686 mclsrcl 30712 mclsval 30714 bj-dmtopon 32242 heibor1lem 32778 heibor 32790 idlval 32982 psubspset 34048 paddfval 34101 pclfvalN 34193 polfvalN 34208 psubclsetN 34240 docafvalN 35429 djafvalN 35441 dicval 35483 dochfval 35657 djhfval 35704 islpolN 35790 mzpclval 36306 eldiophb 36338 rpnnen3 36617 dfac11 36650 rgspnval 36757 clsk1independent 37364 dmvolsal 39240 ovnval 39431 smfresal 39673 issubmgm 41579 lincop 41991 setrec2fun 42238 vsetrec 42245 elpglem3 42255 |
Copyright terms: Public domain | W3C validator |