Theorem elelpwi 4566

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-pw 4558

This theorem is used by:  unipw  5417  axdc2lem  10529  axdc3lem4  10534  homarel  18216  txdis  23956  uhgredgrnv  29713  fpwrelmap  33371  insiga  34816  measinblem  34899  ddemeas  34915  imambfm  34940  totprobd  35104  dstrvprob  35150  ballotlem2  35167  requad2  48814  scmsuppss  49576  lincvalsc0  49626  linc0scn0  49628  lincdifsn  49629  linc1  49630  lincsum  49634  lincscm  49635  lcoss  49641  lincext3  49661  islindeps2  49688  itscnhlinecirc02p  49990