Theorem elpwinss 45043

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3913   ⊆ wss 3914  𝒫 cpw 4563

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 3449  df-in 3921  df-ss 3931  df-pw 4565

This theorem is referenced by:  sge0z  46373  sge0revalmpt  46376  sge0f1o  46380  sge0rnbnd  46391  sge0pnffigt  46394  sge0lefi  46396  sge0ltfirp  46398  sge0gerpmpt  46400  sge0le  46405  sge0ltfirpmpt  46406  sge0iunmptlemre  46413  sge0rpcpnf  46419  sge0lefimpt  46421  sge0ltfirpmpt2  46424  sge0isum  46425  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0pnffigtmpt  46438  sge0pnffsumgt  46440  sge0gtfsumgt  46441  sge0uzfsumgt  46442  sge0seq  46444  sge0reuz  46445  omeiunltfirp  46517  carageniuncllem2  46520  caratheodorylem2  46525