Theorem elelpwi 4542

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-pw 4532

This theorem is referenced by:  unipw  5360  axdc2lem  10135  axdc3lem4  10140  homarel  17667  txdis  22691  uhgredgrnv  27403  fpwrelmap  30970  insiga  32005  measinblem  32088  ddemeas  32104  imambfm  32129  totprobd  32293  dstrvprob  32338  ballotlem2  32355  requad2  44963  scmsuppss  45596  lincvalsc0  45650  linc0scn0  45652  lincdifsn  45653  linc1  45654  lincsum  45658  lincscm  45659  lcoss  45665  lincext3  45685  islindeps2  45712  itscnhlinecirc02p  46019