Theorem elpwinss 45050

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3916   ⊆ wss 3917  𝒫 cpw 4566

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934  df-pw 4568

This theorem is referenced by:  sge0z  46380  sge0revalmpt  46383  sge0f1o  46387  sge0rnbnd  46398  sge0pnffigt  46401  sge0lefi  46403  sge0ltfirp  46405  sge0gerpmpt  46407  sge0le  46412  sge0ltfirpmpt  46413  sge0iunmptlemre  46420  sge0rpcpnf  46426  sge0lefimpt  46428  sge0ltfirpmpt2  46431  sge0isum  46432  sge0xaddlem1  46438  sge0xaddlem2  46439  sge0pnffigtmpt  46445  sge0pnffsumgt  46447  sge0gtfsumgt  46448  sge0uzfsumgt  46449  sge0seq  46451  sge0reuz  46452  omeiunltfirp  46524  carageniuncllem2  46527  caratheodorylem2  46532