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 4547 | . . 3 ⊢ (𝐵 ∈ 𝒫 𝐶 → 𝐵 ⊆ 𝐶) | |
2 | 1 | sseld 3963 | . 2 ⊢ (𝐵 ∈ 𝒫 𝐶 → (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶)) |
3 | 2 | impcom 408 | 1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2105 𝒫 cpw 4535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-in 3940 df-ss 3949 df-pw 4537 |
This theorem is referenced by: unipw 5333 axdc2lem 9858 axdc3lem4 9863 homarel 17284 txdis 22168 uhgredgrnv 26842 fpwrelmap 30395 insiga 31295 measinblem 31378 ddemeas 31394 imambfm 31419 totprobd 31583 dstrvprob 31628 ballotlem2 31645 requad2 43665 scmsuppss 44348 lincvalsc0 44404 linc0scn0 44406 lincdifsn 44407 linc1 44408 lincsum 44412 lincscm 44413 lcoss 44419 lincext3 44439 islindeps2 44466 itscnhlinecirc02p 44700 |
Copyright terms: Public domain | W3C validator |