Theorem elpwinss 45810

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3907   ⊆ wss 3908  𝒫 cpw 4567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925  df-pw 4569

This theorem is used by:  sge0z  47130  sge0revalmpt  47133  sge0f1o  47137  sge0rnbnd  47148  sge0pnffigt  47151  sge0lefi  47153  sge0ltfirp  47155  sge0gerpmpt  47157  sge0le  47162  sge0ltfirpmpt  47163  sge0iunmptlemre  47170  sge0rpcpnf  47176  sge0lefimpt  47178  sge0ltfirpmpt2  47181  sge0isum  47182  sge0xaddlem1  47188  sge0xaddlem2  47189  sge0pnffigtmpt  47195  sge0pnffsumgt  47197  sge0gtfsumgt  47198  sge0uzfsumgt  47199  sge0seq  47201  sge0reuz  47202  omeiunltfirp  47274  carageniuncllem2  47277  caratheodorylem2  47282