![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elpw2 | Structured version Visualization version GIF version |
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |
Ref | Expression |
---|---|
elpw2.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
elpw2 | ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpw2.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | elpw2g 5211 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∈ wcel 2111 Vcvv 3441 ⊆ wss 3881 𝒫 cpw 4497 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 ax-sep 5167 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1541 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-rab 3115 df-v 3443 df-in 3888 df-ss 3898 df-pw 4499 |
This theorem is referenced by: elpwi2 5213 axpweq 5230 knatar 7089 dffi3 8879 marypha1lem 8881 r1pwss 9197 rankr1bg 9216 pwwf 9220 unwf 9223 rankval2 9231 uniwf 9232 rankpwi 9236 dfac2a 9540 dfac12lem2 9555 axdc4lem 9866 axdclem 9930 incexclem 15183 rpnnen2lem1 15559 rpnnen2lem2 15560 sadfval 15791 smufval 15816 smupf 15817 vdwapf 16298 prdshom 16732 mreacs 16921 acsfn 16922 lubeldm 17583 lubval 17586 glbeldm 17596 glbval 17599 clatlem 17713 clatlubcl2 17715 clatglbcl2 17717 issubm 17960 issubg 18271 cntzval 18443 sylow1lem2 18716 lsmvalx 18756 pj1fval 18812 issubrg 19528 islss 19699 lspval 19740 lspcl 19741 islbs 19841 lbsextlem1 19923 lbsextlem3 19925 lbsextlem4 19926 sraval 19941 ocvval 20356 isobs 20409 islinds 20498 aspval 20559 uncmp 22008 cmpfi 22013 cmpfii 22014 2ndc1stc 22056 1stcrest 22058 hausllycmp 22099 lly1stc 22101 1stckgenlem 22158 txlly 22241 txnlly 22242 tx1stc 22255 basqtop 22316 tgqtop 22317 alexsubALTlem3 22654 alexsubALTlem4 22655 alexsubALT 22656 cncfval 23493 cnllycmp 23561 ovolficcss 24073 ovolval 24077 ovolicc2 24126 ismbl 24130 mblsplit 24136 voliunlem3 24156 vitalilem4 24215 vitalilem5 24216 dvfval 24500 dvnfval 24525 cpnfval 24535 plyval 24790 dmarea 25543 wilthlem2 25654 issh 28991 ocval 29063 spanval 29116 hsupval 29117 sshjval 29133 sshjval3 29137 zarcls 31227 zartopn 31228 sigagensiga 31510 dya2iocuni 31651 coinflippv 31851 ballotlemelo 31855 ballotth 31905 erdszelem1 32551 kur14lem9 32574 kur14 32576 cnllysconn 32605 elmpst 32896 mclsrcl 32921 mclsval 32923 icoreresf 34769 cntotbnd 35234 heibor1lem 35247 heibor 35259 isidl 35452 igenval 35499 paddval 37094 pclvalN 37186 polvalN 37201 docavalN 38419 djavalN 38431 dicval 38472 dochval 38647 djhval 38694 lpolconN 38783 elpwbi 39410 elmzpcl 39667 eldiophb 39698 rpnnen3 39973 islssfgi 40016 hbt 40074 elmnc 40080 itgoval 40105 itgocn 40108 rgspnval 40112 issubmgm 44409 elpglem2 45241 |
Copyright terms: Public domain | W3C validator |