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 3401 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | elpw 4489 | 1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∈ wcel 2113 ⊆ wss 3841 𝒫 cpw 4485 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-in 3848 df-ss 3858 df-pw 4487 |
This theorem is referenced by: elpwgOLD 4492 sspw 4498 pwss 4510 snsspw 4727 pwpr 4787 pwtp 4788 pwv 4790 pwuni 4832 sspwuni 4982 iinpw 4988 iunpwss 4989 ssextss 5309 pwin 5419 pwunssOLD 5420 sorpsscmpl 7472 iunpw 7506 ordpwsuc 7543 fabexg 7658 abexssex 7689 qsss 8382 fsetsspwxp 8456 mapval2 8475 pmsspw 8480 uniixp 8524 fineqvlem 8804 fival 8942 hartogslem1 9072 tskwe 9445 cfval2 9753 cflim3 9755 cflim2 9756 cfslb 9759 compsscnvlem 9863 fin1a2lem13 9905 axdc3lem 9943 fpwwe2lem1 10124 fpwwe2lem10 10133 fpwwe2lem11 10134 fpwwe 10139 canthwe 10144 axgroth5 10317 axgroth6 10321 wuncn 10663 ishashinf 13908 vdwmc 16407 ramub2 16443 ram0 16451 restsspw 16801 ismred 16969 mremre 16971 acsfn 17026 submacs 18100 subgacs 18424 nsgacs 18425 sylow2alem2 18854 sylow2a 18855 dprdres 19262 subgdmdprd 19268 pgpfac1lem5 19313 subrgmre 19671 subsubrg2 19674 sdrgacs 19692 lssintcl 19848 lssmre 19850 lssacs 19851 cssmre 20502 istopon 21656 isbasis2g 21692 tgval2 21700 unitg 21711 distop 21739 cldss2 21774 ntreq0 21821 discld 21833 neisspw 21851 restdis 21922 cnntr 22019 isnrm2 22102 cmpcovf 22135 fincmp 22137 cmpsublem 22143 cmpsub 22144 cmpcld 22146 cmpfi 22152 is1stc2 22186 2ndcdisj 22200 llyi 22218 nllyi 22219 nlly2i 22220 llynlly 22221 subislly 22225 restnlly 22226 llyrest 22229 llyidm 22232 nllyidm 22233 islocfin 22261 ptuni2 22320 prdstopn 22372 qtoptop2 22443 qtopuni 22446 tgqtop 22456 isfbas2 22579 isfild 22602 elfg 22615 cfinfil 22637 csdfil 22638 supfil 22639 isufil2 22652 filssufilg 22655 uffix 22665 ufildr 22675 fin1aufil 22676 alexsubb 22790 alexsubALTlem1 22791 alexsubALTlem2 22792 alexsubALT 22795 ptcmplem5 22800 cldsubg 22855 ustfn 22946 ustfilxp 22957 ustn0 22965 dscopn 23319 voliunlem2 24296 vitali 24358 nbuhgr 27277 nbuhgr2vtx1edgblem 27285 shex 29139 dfch2 29334 fpwrelmap 30635 xrsclat 30858 cmpcref 31364 sigaex 31640 sigaval 31641 insiga 31667 sigapisys 31685 sigaldsys 31689 measdivcst 31754 ballotlem2 32017 erdszelem7 32722 erdsze2lem2 32729 rellysconn 32776 dffr5 33284 dmscut 33638 madef 33673 neibastop2lem 34179 neibastop3 34181 topmeet 34183 topjoin 34184 neifg 34190 bj-snglss 34772 bj-pw0ALT 34834 bj-restpw 34873 bj-imdirval2lem 34963 bj-imdiridlem 34966 dissneqlem 35123 topdifinfeq 35133 pibt2 35200 heibor1lem 35579 psubspset 37370 psubclsetN 37562 lcdlss 39245 ismrcd1 40076 pw2f1ocnv 40415 filnm 40471 hbtlem6 40510 elmapintrab 40713 clcnvlem 40760 psshepw 40926 sprsymrelfo 44467 uspgrsprfo 44828 submgmacs 44876 setrec2fun 45835 setrecsres 45844 |
Copyright terms: Public domain | W3C validator |