Theorem elpwinss 45073

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3925   ⊆ wss 3926  𝒫 cpw 4575

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943  df-pw 4577

This theorem is referenced by:  sge0z  46404  sge0revalmpt  46407  sge0f1o  46411  sge0rnbnd  46422  sge0pnffigt  46425  sge0lefi  46427  sge0ltfirp  46429  sge0gerpmpt  46431  sge0le  46436  sge0ltfirpmpt  46437  sge0iunmptlemre  46444  sge0rpcpnf  46450  sge0lefimpt  46452  sge0ltfirpmpt2  46455  sge0isum  46456  sge0xaddlem1  46462  sge0xaddlem2  46463  sge0pnffigtmpt  46469  sge0pnffsumgt  46471  sge0gtfsumgt  46472  sge0uzfsumgt  46473  sge0seq  46475  sge0reuz  46476  omeiunltfirp  46548  carageniuncllem2  46551  caratheodorylem2  46556