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 4754 | . 2 ⊢ (𝐵 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∈ wcel 1977 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-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 |
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-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 |
This theorem is referenced by: axpweq 4768 knatar 6507 canth 6508 dffi3 8220 marypha1lem 8222 r1pwss 8530 rankr1bg 8549 pwwf 8553 unwf 8556 rankval2 8564 uniwf 8565 rankpwi 8569 aceq3lem 8826 dfac2a 8835 dfac12lem2 8849 axdc3lem4 9158 axdc4lem 9160 axdclem 9224 grothpw 9527 uzf 11566 ixxf 12056 fzf 12201 incexclem 14407 rpnnen2lem1 14782 rpnnen2lem2 14783 bitsf 14987 sadfval 15012 smufval 15037 smupf 15038 vdwapf 15514 prdsval 15938 prdsds 15947 prdshom 15950 mreacs 16142 acsfn 16143 wunnat 16439 lubeldm 16804 lubval 16807 glbeldm 16817 glbval 16820 clatlem 16934 clatlubcl2 16936 clatglbcl2 16938 issubm 17170 issubg 17417 cntzval 17577 sylow1lem2 17837 lsmvalx 17877 pj1fval 17930 issubrg 18603 islss 18756 lspval 18796 lspcl 18797 islbs 18897 lbsextlem1 18979 lbsextlem3 18981 lbsextlem4 18982 sraval 18997 aspval 19149 ocvfval 19829 ocvval 19830 isobs 19883 islinds 19967 leordtval2 20826 cnpfval 20848 iscnp2 20853 uncmp 21016 cmpfi 21021 cmpfii 21022 2ndc1stc 21064 1stcrest 21066 islly2 21097 hausllycmp 21107 lly1stc 21109 1stckgenlem 21166 xkotf 21198 txlly 21249 txnlly 21250 tx1stc 21263 basqtop 21324 tgqtop 21325 alexsubALTlem3 21663 alexsubALTlem4 21664 alexsubALT 21665 sszcld 22428 cncfval 22499 cnllycmp 22563 bndth 22565 ishtpy 22579 ovolficcss 23045 ovolval 23049 ovolicc2 23097 ismbl 23101 mblsplit 23107 voliunlem3 23127 vitalilem4 23186 vitalilem5 23187 dvfval 23467 dvnfval 23491 cpnfval 23501 plyval 23753 dmarea 24484 wilthlem2 24595 umgrabi 26510 issh 27449 ocval 27523 spanval 27576 hsupval 27577 sshjval 27593 sshjval3 27597 fpwrelmap 28896 sigagensiga 29531 dya2iocuni 29672 coinflippv 29872 ballotlemelo 29876 ballotlem2 29877 ballotth 29926 erdszelem1 30427 kur14lem9 30450 kur14 30452 cnllyscon 30481 elmpst 30687 mclsrcl 30712 mclsval 30714 icoreresf 32376 cover2 32678 cntotbnd 32765 heibor1lem 32778 heibor 32790 isidl 32983 igenval 33030 paddval 34102 pclvalN 34194 polvalN 34209 docavalN 35430 djavalN 35442 dicval 35483 dochval 35658 djhval 35705 lpolconN 35794 elmzpcl 36307 eldiophb 36338 rpnnen3 36617 islssfgi 36660 hbt 36719 elmnc 36725 itgoval 36750 itgocn 36753 rgspnval 36757 issubmgm 41579 elpglem2 42254 |
Copyright terms: Public domain | W3C validator |