| 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 3484 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | 1 | elpw 4604 | 1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 ⊆ wss 3951 𝒫 cpw 4600 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-pw 4602 |
| This theorem is referenced by: sspw 4611 pwss 4623 snsspw 4844 pwpr 4901 pwtp 4902 pwv 4904 pwuni 4945 sspwuni 5100 iinpw 5106 iunpwss 5107 ssextss 5458 pwin 5574 dffr6 5640 sorpsscmpl 7754 iunpw 7791 ordpwsuc 7835 fabexd 7959 fabexgOLD 7961 abexssex 7995 qsss 8818 fsetsspwxp 8893 mapval2 8912 pmsspw 8917 uniixp 8961 fineqvlem 9298 fival 9452 hartogslem1 9582 tskwe 9990 cfval2 10300 cflim3 10302 cflim2 10303 cfslb 10306 compsscnvlem 10410 fin1a2lem13 10452 axdc3lem 10490 fpwwe2lem1 10671 fpwwe2lem10 10680 fpwwe2lem11 10681 fpwwe 10686 canthwe 10691 axgroth5 10864 axgroth6 10868 wuncn 11210 ishashinf 14502 vdwmc 17016 ramub2 17052 ram0 17060 restsspw 17476 ismred 17645 mremre 17647 acsfn 17702 submgmacs 18730 submacs 18840 subgacs 19179 nsgacs 19180 sylow2alem2 19636 sylow2a 19637 dprdres 20048 subgdmdprd 20054 pgpfac1lem5 20099 subrngmre 20562 subsubrng2 20564 subrgmre 20597 subsubrg2 20599 sdrgacs 20802 lssintcl 20962 lssmre 20964 lssacs 20965 cssmre 21711 istopon 22918 isbasis2g 22955 tgval2 22963 unitg 22974 distop 23002 cldss2 23038 ntreq0 23085 discld 23097 neisspw 23115 restdis 23186 cnntr 23283 isnrm2 23366 cmpcovf 23399 fincmp 23401 cmpsublem 23407 cmpsub 23408 cmpcld 23410 cmpfi 23416 is1stc2 23450 2ndcdisj 23464 llyi 23482 nllyi 23483 nlly2i 23484 llynlly 23485 subislly 23489 restnlly 23490 llyrest 23493 llyidm 23496 nllyidm 23497 islocfin 23525 ptuni2 23584 prdstopn 23636 qtoptop2 23707 qtopuni 23710 tgqtop 23720 isfbas2 23843 isfild 23866 elfg 23879 cfinfil 23901 csdfil 23902 supfil 23903 isufil2 23916 filssufilg 23919 uffix 23929 ufildr 23939 fin1aufil 23940 alexsubb 24054 alexsubALTlem1 24055 alexsubALTlem2 24056 alexsubALT 24059 ptcmplem5 24064 cldsubg 24119 ustfn 24210 ustfilxp 24221 ustn0 24229 dscopn 24586 voliunlem2 25586 vitali 25648 dmscut 27856 madef 27895 nbuhgr 29360 nbuhgr2vtx1edgblem 29368 shex 31231 dfch2 31426 fpwrelmap 32744 xrsclat 33013 cmpcref 33849 sigaex 34111 sigaval 34112 insiga 34138 sigapisys 34156 sigaldsys 34160 measdivcst 34225 ballotlem2 34491 erdszelem7 35202 erdsze2lem2 35209 rellysconn 35256 dffr5 35754 neibastop2lem 36361 neibastop3 36363 topmeet 36365 topjoin 36366 neifg 36372 bj-snglss 36971 bj-pw0ALT 37050 bj-restpw 37093 bj-imdirval2lem 37183 bj-imdiridlem 37186 dissneqlem 37341 topdifinfeq 37351 pibt2 37418 heibor1lem 37816 psubspset 39746 psubclsetN 39938 lcdlss 41621 ismrcd1 42709 pw2f1ocnv 43049 filnm 43102 hbtlem6 43141 dfno2 43441 elmapintrab 43589 clcnvlem 43636 psshepw 43801 ssclaxsep 44999 pwclaxpow 45001 sprsymrelfo 47484 uspgrsprfo 48064 setrec2fun 49211 setrecsres 49221 |
| Copyright terms: Public domain | W3C validator |