Theorem elelpwi 4615

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2106  𝒫 cpw 4605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-pw 4607

This theorem is referenced by:  unipw  5461  axdc2lem  10486  axdc3lem4  10491  homarel  18090  txdis  23656  uhgredgrnv  29162  fpwrelmap  32751  insiga  34118  measinblem  34201  ddemeas  34217  imambfm  34244  totprobd  34408  dstrvprob  34453  ballotlem2  34470  requad2  47548  scmsuppss  48216  lincvalsc0  48267  linc0scn0  48269  lincdifsn  48270  linc1  48271  lincsum  48275  lincscm  48276  lcoss  48282  lincext3  48302  islindeps2  48329  itscnhlinecirc02p  48635