Theorem elelpwi 4546

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ss 3907  df-pw 4538

This theorem is referenced by:  unipw  5396  axdc2lem  10368  axdc3lem4  10373  homarel  18001  txdis  23622  uhgredgrnv  29224  fpwrelmap  32832  insiga  34328  measinblem  34411  ddemeas  34427  imambfm  34453  totprobd  34617  dstrvprob  34663  ballotlem2  34680  requad2  48121  scmsuppss  48869  lincvalsc0  48919  linc0scn0  48921  lincdifsn  48922  linc1  48923  lincsum  48927  lincscm  48928  lcoss  48934  lincext3  48954  islindeps2  48981  itscnhlinecirc02p  49283