Theorem elelpwi 4510

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 4507	. . 3 ⊢ (𝐵 ∈ 𝒫 𝐶 → 𝐵 ⊆ 𝐶)
2	1	sseld 3894	. 2 ⊢ (𝐵 ∈ 𝒫 𝐶 → (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶))
3	2	impcom 411	1 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝒫 𝐶) → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112  𝒫 cpw 4498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-v 3412  df-in 3868  df-ss 3878  df-pw 4500

This theorem is referenced by:  unipw  5316  axdc2lem  9922  axdc3lem4  9927  homarel  17377  txdis  22347  uhgredgrnv  27037  fpwrelmap  30606  insiga  31638  measinblem  31721  ddemeas  31737  imambfm  31762  totprobd  31926  dstrvprob  31971  ballotlem2  31988  requad2  44568  scmsuppss  45201  lincvalsc0  45255  linc0scn0  45257  lincdifsn  45258  linc1  45259  lincsum  45263  lincscm  45264  lcoss  45270  lincext3  45290  islindeps2  45317  itscnhlinecirc02p  45624