Theorem elelpwi 4632

Description: If 𝐴 belongs to a part of 𝐶, then 𝐴 belongs to 𝐶. (Contributed by FL, 3-Aug-2009.)

Assertion

Ref	Expression
elelpwi	⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶)

Proof of Theorem elelpwi

Step	Hyp	Ref	Expression
1		elpwi 4629	. . 3 ⊢ (𝐵 ∈ 𝒫 𝐶 → 𝐵 ⊆ 𝐶)
2	1	sseld 4007	. 2 ⊢ (𝐵 ∈ 𝒫 𝐶 → (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶))
3	2	impcom 407	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  𝒫 cpw 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ss 3993  df-pw 4624

This theorem is referenced by:  unipw  5470  axdc2lem  10517  axdc3lem4  10522  homarel  18103  txdis  23661  uhgredgrnv  29165  fpwrelmap  32747  insiga  34101  measinblem  34184  ddemeas  34200  imambfm  34227  totprobd  34391  dstrvprob  34436  ballotlem2  34453  requad2  47497  scmsuppss  48097  lincvalsc0  48150  linc0scn0  48152  lincdifsn  48153  linc1  48154  lincsum  48158  lincscm  48159  lcoss  48165  lincext3  48185  islindeps2  48212  itscnhlinecirc02p  48519