Theorem elelpwi 4564

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  𝒫 cpw 4554

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ss 3918  df-pw 4556

This theorem is referenced by:  unipw  5398  axdc2lem  10358  axdc3lem4  10363  homarel  17960  txdis  23576  uhgredgrnv  29203  fpwrelmap  32812  insiga  34294  measinblem  34377  ddemeas  34393  imambfm  34419  totprobd  34583  dstrvprob  34629  ballotlem2  34646  requad2  47865  scmsuppss  48613  lincvalsc0  48663  linc0scn0  48665  lincdifsn  48666  linc1  48667  lincsum  48671  lincscm  48672  lcoss  48678  lincext3  48698  islindeps2  48725  itscnhlinecirc02p  49027