Theorem elpwinss 45403

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3902   ⊆ wss 3903  𝒫 cpw 4556

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by:  sge0z  46727  sge0revalmpt  46730  sge0f1o  46734  sge0rnbnd  46745  sge0pnffigt  46748  sge0lefi  46750  sge0ltfirp  46752  sge0gerpmpt  46754  sge0le  46759  sge0ltfirpmpt  46760  sge0iunmptlemre  46767  sge0rpcpnf  46773  sge0lefimpt  46775  sge0ltfirpmpt2  46778  sge0isum  46779  sge0xaddlem1  46785  sge0xaddlem2  46786  sge0pnffigtmpt  46792  sge0pnffsumgt  46794  sge0gtfsumgt  46795  sge0uzfsumgt  46796  sge0seq  46798  sge0reuz  46799  omeiunltfirp  46871  carageniuncllem2  46874  caratheodorylem2  46879