Theorem elelpwi 4568

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  𝒫 cpw 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ss 3924  df-pw 4560

This theorem is referenced by:  unipw  5422  axdc2lem  10420  axdc3lem4  10425  homarel  18083  txdis  23750  uhgredgrnv  29389  fpwrelmap  32990  insiga  34444  measinblem  34527  ddemeas  34543  imambfm  34569  totprobd  34733  dstrvprob  34779  ballotlem2  34796  requad2  48243  scmsuppss  49002  lincvalsc0  49052  linc0scn0  49054  lincdifsn  49055  linc1  49056  lincsum  49060  lincscm  49061  lcoss  49067  lincext3  49087  islindeps2  49114  itscnhlinecirc02p  49416