![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elelpwi | Structured version Visualization version GIF version |
Description: If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.) |
Ref | Expression |
---|---|
elelpwi | ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi 4608 | . . 3 ⊢ (𝐵 ∈ 𝒫 𝐶 → 𝐵 ⊆ 𝐶) | |
2 | 1 | sseld 3980 | . 2 ⊢ (𝐵 ∈ 𝒫 𝐶 → (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶)) |
3 | 2 | impcom 408 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 𝒫 cpw 4601 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3954 df-ss 3964 df-pw 4603 |
This theorem is referenced by: unipw 5449 axdc2lem 10439 axdc3lem4 10444 homarel 17982 txdis 23127 uhgredgrnv 28379 fpwrelmap 31945 insiga 33123 measinblem 33206 ddemeas 33222 imambfm 33249 totprobd 33413 dstrvprob 33458 ballotlem2 33475 requad2 46277 scmsuppss 47001 lincvalsc0 47055 linc0scn0 47057 lincdifsn 47058 linc1 47059 lincsum 47063 lincscm 47064 lcoss 47070 lincext3 47090 islindeps2 47117 itscnhlinecirc02p 47424 |
Copyright terms: Public domain | W3C validator |