Theorem elpwinss 45801

Description: An element of the powerset of 𝐵 intersected with anything, is a subset of 𝐵. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
elpwinss	⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Proof of Theorem elpwinss

Step	Hyp	Ref	Expression
1		elinel1 4157	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ∈ 𝒫 𝐵)
2	1	elpwid 4574	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925  df-pw 4567

This theorem is used by:  sge0z  47121  sge0revalmpt  47124  sge0f1o  47128  sge0rnbnd  47139  sge0pnffigt  47142  sge0lefi  47144  sge0ltfirp  47146  sge0gerpmpt  47148  sge0le  47153  sge0ltfirpmpt  47154  sge0iunmptlemre  47161  sge0rpcpnf  47167  sge0lefimpt  47169  sge0ltfirpmpt2  47172  sge0isum  47173  sge0xaddlem1  47179  sge0xaddlem2  47180  sge0pnffigtmpt  47186  sge0pnffsumgt  47188  sge0gtfsumgt  47189  sge0uzfsumgt  47190  sge0seq  47192  sge0reuz  47193  omeiunltfirp  47265  carageniuncllem2  47268  caratheodorylem2  47273