Theorem elpwinss 45027

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ss 3922  df-pw 4555

This theorem is referenced by:  sge0z  46357  sge0revalmpt  46360  sge0f1o  46364  sge0rnbnd  46375  sge0pnffigt  46378  sge0lefi  46380  sge0ltfirp  46382  sge0gerpmpt  46384  sge0le  46389  sge0ltfirpmpt  46390  sge0iunmptlemre  46397  sge0rpcpnf  46403  sge0lefimpt  46405  sge0ltfirpmpt2  46408  sge0isum  46409  sge0xaddlem1  46415  sge0xaddlem2  46416  sge0pnffigtmpt  46422  sge0pnffsumgt  46424  sge0gtfsumgt  46425  sge0uzfsumgt  46426  sge0seq  46428  sge0reuz  46429  omeiunltfirp  46501  carageniuncllem2  46504  caratheodorylem2  46509