Theorem elpwinss 45504

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

Syntax hints:   → wi 4   ∈ wcel 2119   ∩ cin 3889   ⊆ wss 3890  𝒫 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-v 3434  df-in 3897  df-ss 3907  df-pw 4538

This theorem is referenced by:  sge0z  46825  sge0revalmpt  46828  sge0f1o  46832  sge0rnbnd  46843  sge0pnffigt  46846  sge0lefi  46848  sge0ltfirp  46850  sge0gerpmpt  46852  sge0le  46857  sge0ltfirpmpt  46858  sge0iunmptlemre  46865  sge0rpcpnf  46871  sge0lefimpt  46873  sge0ltfirpmpt2  46876  sge0isum  46877  sge0xaddlem1  46883  sge0xaddlem2  46884  sge0pnffigtmpt  46890  sge0pnffsumgt  46892  sge0gtfsumgt  46893  sge0uzfsumgt  46894  sge0seq  46896  sge0reuz  46897  omeiunltfirp  46969  carageniuncllem2  46972  caratheodorylem2  46977