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 5247 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∈ wcel 2114 Vcvv 3494 ⊆ wss 3936 𝒫 cpw 4539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-in 3943 df-ss 3952 df-pw 4541 |
This theorem is referenced by: axpweq 5265 knatar 7110 dffi3 8895 marypha1lem 8897 r1pwss 9213 rankr1bg 9232 pwwf 9236 unwf 9239 rankval2 9247 uniwf 9248 rankpwi 9252 dfac2a 9555 dfac12lem2 9570 axdc4lem 9877 axdclem 9941 incexclem 15191 rpnnen2lem1 15567 rpnnen2lem2 15568 sadfval 15801 smufval 15826 smupf 15827 vdwapf 16308 prdshom 16740 mreacs 16929 acsfn 16930 lubeldm 17591 lubval 17594 glbeldm 17604 glbval 17607 clatlem 17721 clatlubcl2 17723 clatglbcl2 17725 issubm 17968 issubg 18279 cntzval 18451 sylow1lem2 18724 lsmvalx 18764 pj1fval 18820 issubrg 19535 islss 19706 lspval 19747 lspcl 19748 islbs 19848 lbsextlem1 19930 lbsextlem3 19932 lbsextlem4 19933 sraval 19948 aspval 20102 ocvval 20811 isobs 20864 islinds 20953 uncmp 22011 cmpfi 22016 cmpfii 22017 2ndc1stc 22059 1stcrest 22061 hausllycmp 22102 lly1stc 22104 1stckgenlem 22161 txlly 22244 txnlly 22245 tx1stc 22258 basqtop 22319 tgqtop 22320 alexsubALTlem3 22657 alexsubALTlem4 22658 alexsubALT 22659 cncfval 23496 cnllycmp 23560 ovolficcss 24070 ovolval 24074 ovolicc2 24123 ismbl 24127 mblsplit 24133 voliunlem3 24153 vitalilem4 24212 vitalilem5 24213 dvfval 24495 dvnfval 24519 cpnfval 24529 plyval 24783 dmarea 25535 wilthlem2 25646 issh 28985 ocval 29057 spanval 29110 hsupval 29111 sshjval 29127 sshjval3 29131 sigagensiga 31400 dya2iocuni 31541 coinflippv 31741 ballotlemelo 31745 ballotth 31795 erdszelem1 32438 kur14lem9 32461 kur14 32463 cnllysconn 32492 elmpst 32783 mclsrcl 32808 mclsval 32810 icoreresf 34636 cntotbnd 35089 heibor1lem 35102 heibor 35114 isidl 35307 igenval 35354 paddval 36949 pclvalN 37041 polvalN 37056 docavalN 38274 djavalN 38286 dicval 38327 dochval 38502 djhval 38549 lpolconN 38638 elpwbi 39136 elmzpcl 39343 eldiophb 39374 rpnnen3 39649 islssfgi 39692 hbt 39750 elmnc 39756 itgoval 39781 itgocn 39784 rgspnval 39788 issubmgm 44076 elpglem2 44834 |
Copyright terms: Public domain | W3C validator |