Theorem elpwinss 42056

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3857   ⊆ wss 3858  𝒫 cpw 4494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875  df-pw 4496

This theorem is referenced by:  sge0z  43380  sge0revalmpt  43383  sge0f1o  43387  sge0rnbnd  43398  sge0pnffigt  43401  sge0lefi  43403  sge0ltfirp  43405  sge0gerpmpt  43407  sge0le  43412  sge0ltfirpmpt  43413  sge0iunmptlemre  43420  sge0rpcpnf  43426  sge0lefimpt  43428  sge0ltfirpmpt2  43431  sge0isum  43432  sge0xaddlem1  43438  sge0xaddlem2  43439  sge0pnffigtmpt  43445  sge0pnffsumgt  43447  sge0gtfsumgt  43448  sge0uzfsumgt  43449  sge0seq  43451  sge0reuz  43452  omeiunltfirp  43524  carageniuncllem2  43527  caratheodorylem2  43532