Theorem elpwinss 46009

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898   ⊆ wss 3899  𝒫 cpw 4557

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916  df-pw 4559

This theorem is used by:  sge0z  47329  sge0revalmpt  47332  sge0f1o  47336  sge0rnbnd  47347  sge0pnffigt  47350  sge0lefi  47352  sge0ltfirp  47354  sge0gerpmpt  47356  sge0le  47361  sge0ltfirpmpt  47362  sge0iunmptlemre  47369  sge0rpcpnf  47375  sge0lefimpt  47377  sge0ltfirpmpt2  47380  sge0isum  47381  sge0xaddlem1  47387  sge0xaddlem2  47388  sge0pnffigtmpt  47394  sge0pnffsumgt  47396  sge0gtfsumgt  47397  sge0uzfsumgt  47398  sge0seq  47400  sge0reuz  47401  omeiunltfirp  47473  carageniuncllem2  47476  caratheodorylem2  47481