![]() |
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 5104 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2050 Vcvv 3415 ⊆ wss 3831 𝒫 cpw 4423 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5061 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-v 3417 df-in 3838 df-ss 3845 df-pw 4425 |
This theorem is referenced by: axpweq 5119 knatar 6935 dffi3 8692 marypha1lem 8694 r1pwss 9009 rankr1bg 9028 pwwf 9032 unwf 9035 rankval2 9043 uniwf 9044 rankpwi 9048 dfac2a 9351 dfac12lem2 9366 axdc4lem 9677 axdclem 9741 incexclem 15054 rpnnen2lem1 15430 rpnnen2lem2 15431 sadfval 15664 smufval 15689 smupf 15690 vdwapf 16167 prdshom 16599 mreacs 16790 acsfn 16791 lubeldm 17452 lubval 17455 glbeldm 17465 glbval 17468 clatlem 17582 clatlubcl2 17584 clatglbcl2 17586 issubm 17818 issubg 18066 cntzval 18225 sylow1lem2 18488 lsmvalx 18528 pj1fval 18581 issubrg 19261 islss 19431 lspval 19472 lspcl 19473 islbs 19573 lbsextlem1 19655 lbsextlem3 19657 lbsextlem4 19658 sraval 19673 aspval 19825 ocvval 20516 isobs 20569 islinds 20658 uncmp 21718 cmpfi 21723 cmpfii 21724 2ndc1stc 21766 1stcrest 21768 hausllycmp 21809 lly1stc 21811 1stckgenlem 21868 txlly 21951 txnlly 21952 tx1stc 21965 basqtop 22026 tgqtop 22027 alexsubALTlem3 22364 alexsubALTlem4 22365 alexsubALT 22366 cncfval 23202 cnllycmp 23266 ovolficcss 23776 ovolval 23780 ovolicc2 23829 ismbl 23833 mblsplit 23839 voliunlem3 23859 vitalilem4 23918 vitalilem5 23919 dvfval 24201 dvnfval 24225 cpnfval 24235 plyval 24489 dmarea 25240 wilthlem2 25351 issh 28767 ocval 28841 spanval 28894 hsupval 28895 sshjval 28911 sshjval3 28915 fpwrelmap 30224 sigagensiga 31045 dya2iocuni 31186 coinflippv 31387 ballotlemelo 31391 ballotth 31441 erdszelem1 32023 kur14lem9 32046 kur14 32048 cnllysconn 32077 elmpst 32303 mclsrcl 32328 mclsval 32330 icoreresf 34075 cntotbnd 34516 heibor1lem 34529 heibor 34541 isidl 34734 igenval 34781 paddval 36379 pclvalN 36471 polvalN 36486 docavalN 37704 djavalN 37716 dicval 37757 dochval 37932 djhval 37979 lpolconN 38068 elpwbi 38561 elmzpcl 38718 eldiophb 38749 rpnnen3 39025 islssfgi 39068 hbt 39126 elmnc 39132 itgoval 39157 itgocn 39160 rgspnval 39164 issubmgm 43425 elpglem2 44182 |
Copyright terms: Public domain | W3C validator |