| 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 3457 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | 1 | elpw 4556 | 1 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 208 ∈ wcel 2141 ⊆ wss 3902 𝒫 cpw 4552 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-tru 1562 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-v 3455 df-ss 3919 df-pw 4554 |
| This theorem is referenced by: sspw 4563 pwss 4576 snsspw 4799 pwpr 4856 pwtp 4857 pwv 4859 pwuni 4901 sspwuni 5054 iinpw 5060 iunpwss 5061 ssextss 5417 pwin 5534 dffr6 5599 sorpsscmpl 7712 iunpw 7749 ordpwsuc 7790 fabexd 7913 abexssex 7946 qsss 8751 fsetsspwxp 8828 mapval2 8848 pmsspw 8853 uniixp 8897 fineqvlem 9204 fival 9352 hartogslem1 9484 tskwe 9902 cfval2 10211 cflim3 10213 cflim2 10214 cfslb 10217 compsscnvlem 10321 fin1a2lem13 10363 axdc3lem 10401 fpwwe2lem1 10583 fpwwe2lem10 10592 fpwwe2lem11 10593 fpwwe 10598 canthwe 10603 axgroth5 10776 axgroth6 10780 wuncn 11122 ishashinf 14470 vdwmc 17005 ramub2 17041 ram0 17049 restsspw 17451 ismred 17621 mremre 17623 acsfn 17682 submgmacs 18742 submacs 18852 subgacs 19193 nsgacs 19194 sylow2alem2 19649 sylow2a 19650 dprdres 20061 subgdmdprd 20067 pgpfac1lem5 20112 subrngmre 20599 subsubrng2 20601 subrgmre 20634 subsubrg2 20636 sdrgacs 20838 lssintcl 21019 lssmre 21021 lssacs 21022 cssmre 21733 istopon 22960 isbasis2g 22996 tgval2 23004 unitg 23015 distop 23043 cldss2 23078 ntreq0 23125 discld 23137 neisspw 23155 restdis 23226 cnntr 23323 isnrm2 23406 cmpcovf 23439 fincmp 23441 cmpsublem 23447 cmpsub 23448 cmpcld 23450 cmpfi 23456 is1stc2 23490 2ndcdisj 23504 llyi 23522 nllyi 23523 nlly2i 23524 llynlly 23525 subislly 23529 restnlly 23530 llyrest 23533 llyidm 23536 nllyidm 23537 islocfin 23565 ptuni2 23624 prdstopn 23676 qtoptop2 23747 qtopuni 23750 tgqtop 23760 isfbas2 23883 isfild 23906 elfg 23919 cfinfil 23941 csdfil 23942 supfil 23943 isufil2 23956 filssufilg 23959 uffix 23969 ufildr 23979 fin1aufil 23980 alexsubb 24094 alexsubALTlem1 24095 alexsubALTlem2 24096 alexsubALT 24099 ptcmplem5 24104 cldsubg 24159 ustfn 24250 ustfilxp 24261 ustn0 24269 dscopn 24621 voliunlem2 25601 vitali 25663 dmcuts 27872 madef 27917 nbuhgr 29501 nbuhgr2vtx1edgblem 29509 shex 31372 dfch2 31567 fpwrelmap 32896 xrsclat 33150 cmpcref 34108 sigaex 34368 sigaval 34369 insiga 34395 sigapisys 34413 sigaldsys 34417 measdivcst 34482 ballotlem2 34747 erdszelem7 35508 erdsze2lem2 35515 rellysconn 35562 dffr5 36065 neibastop2lem 36681 neibastop3 36683 topmeet 36685 topjoin 36686 neifg 36692 mh-infprim2bi 36868 bj-snglss 37416 bj-pw0ALT 37495 bj-restpw 37543 bj-imdirval2lem 37635 bj-imdiridlem 37638 dissneqlem 37795 topdifinfeq 37805 pibt2 37872 heibor1lem 38269 psubspset 40329 psubclsetN 40521 lcdlss 42204 ismrcd1 43240 pw2f1ocnv 43575 filnm 43628 hbtlem6 43667 dfno2 43965 elmapintrab 44113 clcnvlem 44160 psshepw 44325 ssclaxsep 45519 pwclaxpow 45521 sprsymrelfo 48064 uspgrsprfo 48731 setrec2fun 50274 setrecsres 50284 |
| Copyright terms: Public domain | W3C validator |