Theorem elelpwi 4573

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  𝒫 cpw 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ss 3923  df-pw 4565

This theorem is referenced by:  unipw  5433  axdc2lem  10433  axdc3lem4  10438  homarel  18094  txdis  23770  uhgredgrnv  29458  fpwrelmap  33056  insiga  34505  measinblem  34588  ddemeas  34604  imambfm  34630  totprobd  34794  dstrvprob  34840  ballotlem2  34857  requad2  48365  scmsuppss  49128  lincvalsc0  49178  linc0scn0  49180  lincdifsn  49181  linc1  49182  lincsum  49186  lincscm  49187  lcoss  49193  lincext3  49213  islindeps2  49240  itscnhlinecirc02p  49542