Theorem elelpwi 4563

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3922  df-pw 4555

This theorem is referenced by:  unipw  5397  axdc2lem  10361  axdc3lem4  10366  homarel  17961  txdis  23535  uhgredgrnv  29093  fpwrelmap  32689  insiga  34103  measinblem  34186  ddemeas  34202  imambfm  34229  totprobd  34393  dstrvprob  34439  ballotlem2  34456  requad2  47608  scmsuppss  48356  lincvalsc0  48407  linc0scn0  48409  lincdifsn  48410  linc1  48411  lincsum  48415  lincscm  48416  lcoss  48422  lincext3  48442  islindeps2  48469  itscnhlinecirc02p  48771