Theorem elpwinss 46159

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895   ∩ cin 4089  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091  df-pw 4558

This theorem is used by:  sge0z  47478  sge0revalmpt  47481  sge0f1o  47485  sge0rnbnd  47496  sge0pnffigt  47499  sge0lefi  47501  sge0ltfirp  47503  sge0gerpmpt  47505  sge0le  47510  sge0ltfirpmpt  47511  sge0iunmptlemre  47518  sge0rpcpnf  47524  sge0lefimpt  47526  sge0ltfirpmpt2  47529  sge0isum  47530  sge0xaddlem1  47536  sge0xaddlem2  47537  sge0pnffigtmpt  47543  sge0pnffsumgt  47545  sge0gtfsumgt  47546  sge0uzfsumgt  47547  sge0seq  47549  sge0reuz  47550  omeiunltfirp  47622  carageniuncllem2  47625  caratheodorylem2  47630