Theorem elpwinss 43379

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 4160	. 2 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ∈ 𝒫 𝐵)
2	1	elpwid 4574	1 ⊢ (𝐴 ∈ (𝒫 𝐵 ∩ 𝐶) → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3912   ⊆ wss 3913  𝒫 cpw 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567

This theorem is referenced by:  sge0z  44736  sge0revalmpt  44739  sge0f1o  44743  sge0rnbnd  44754  sge0pnffigt  44757  sge0lefi  44759  sge0ltfirp  44761  sge0gerpmpt  44763  sge0le  44768  sge0ltfirpmpt  44769  sge0iunmptlemre  44776  sge0rpcpnf  44782  sge0lefimpt  44784  sge0ltfirpmpt2  44787  sge0isum  44788  sge0xaddlem1  44794  sge0xaddlem2  44795  sge0pnffigtmpt  44801  sge0pnffsumgt  44803  sge0gtfsumgt  44804  sge0uzfsumgt  44805  sge0seq  44807  sge0reuz  44808  omeiunltfirp  44880  carageniuncllem2  44883  caratheodorylem2  44888