Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > velpw | Structured version Visualization version GIF version |
Description: Setvar variable membership in a power class. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
velpw | ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3497 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | elpw 4543 | 1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∈ wcel 2114 ⊆ 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 |
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-v 3496 df-in 3943 df-ss 3952 df-pw 4541 |
This theorem is referenced by: elpwgOLD 4546 sspw 4552 pwss 4564 snsspw 4775 pwpr 4832 pwtp 4833 pwv 4835 pwuni 4875 sspwuni 5022 iinpw 5028 iunpwss 5029 ssextss 5346 pwin 5454 pwunssOLD 5455 sorpsscmpl 7460 iunpw 7493 ordpwsuc 7530 fabexg 7639 abexssex 7671 qsss 8358 mapval2 8436 pmsspw 8441 uniixp 8485 fineqvlem 8732 fival 8876 hartogslem1 9006 tskwe 9379 cfval2 9682 cflim3 9684 cflim2 9685 cfslb 9688 compsscnvlem 9792 fin1a2lem13 9834 axdc3lem 9872 fpwwe2lem1 10053 fpwwe2lem11 10062 fpwwe2lem12 10063 fpwwe 10068 canthwe 10073 axgroth5 10246 axgroth6 10250 wuncn 10592 ishashinf 13822 vdwmc 16314 ramub2 16350 ram0 16358 restsspw 16705 ismred 16873 mremre 16875 acsfn 16930 submacs 17991 subgacs 18313 nsgacs 18314 sylow2alem2 18743 sylow2a 18744 dprdres 19150 subgdmdprd 19156 pgpfac1lem5 19201 subrgmre 19559 subsubrg2 19562 sdrgacs 19580 lssintcl 19736 lssmre 19738 lssacs 19739 cssmre 20837 istopon 21520 isbasis2g 21556 tgval2 21564 unitg 21575 distop 21603 cldss2 21638 ntreq0 21685 discld 21697 neisspw 21715 restdis 21786 cnntr 21883 isnrm2 21966 cmpcovf 21999 fincmp 22001 cmpsublem 22007 cmpsub 22008 cmpcld 22010 cmpfi 22016 is1stc2 22050 2ndcdisj 22064 llyi 22082 nllyi 22083 nlly2i 22084 llynlly 22085 subislly 22089 restnlly 22090 llyrest 22093 llyidm 22096 nllyidm 22097 islocfin 22125 ptuni2 22184 prdstopn 22236 qtoptop2 22307 qtopuni 22310 tgqtop 22320 isfbas2 22443 isfild 22466 elfg 22479 cfinfil 22501 csdfil 22502 supfil 22503 isufil2 22516 filssufilg 22519 uffix 22529 ufildr 22539 fin1aufil 22540 alexsubb 22654 alexsubALTlem1 22655 alexsubALTlem2 22656 alexsubALT 22659 ptcmplem5 22664 cldsubg 22719 ustfn 22810 ustfilxp 22821 ustn0 22829 dscopn 23183 voliunlem2 24152 vitali 24214 nbuhgr 27125 nbuhgr2vtx1edgblem 27133 shex 28989 dfch2 29184 fpwrelmap 30469 xrsclat 30667 cmpcref 31114 sigaex 31369 sigaval 31370 insiga 31396 sigapisys 31414 sigaldsys 31418 measdivcst 31483 ballotlem2 31746 erdszelem7 32444 erdsze2lem2 32451 rellysconn 32498 dffr5 32989 dmscut 33272 neibastop2lem 33708 neibastop3 33710 topmeet 33712 topjoin 33713 neifg 33719 bj-snglss 34285 bj-pw0ALT 34345 bj-restpw 34386 bj-imdirval2 34476 bj-imdirid 34478 dissneqlem 34624 topdifinfeq 34634 pibt2 34701 heibor1lem 35102 psubspset 36895 psubclsetN 37087 lcdlss 38770 ismrcd1 39315 pw2f1ocnv 39654 filnm 39710 hbtlem6 39749 elmapintrab 39956 clcnvlem 40003 psshepw 40154 sprsymrelfo 43679 uspgrsprfo 44043 submgmacs 44091 setrec2fun 44815 setrecsres 44824 |
Copyright terms: Public domain | W3C validator |