Theorem elpwinss 45891

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4560

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919  df-pw 4562

This theorem is used by:  sge0z  47211  sge0revalmpt  47214  sge0f1o  47218  sge0rnbnd  47229  sge0pnffigt  47232  sge0lefi  47234  sge0ltfirp  47236  sge0gerpmpt  47238  sge0le  47243  sge0ltfirpmpt  47244  sge0iunmptlemre  47251  sge0rpcpnf  47257  sge0lefimpt  47259  sge0ltfirpmpt2  47262  sge0isum  47263  sge0xaddlem1  47269  sge0xaddlem2  47270  sge0pnffigtmpt  47276  sge0pnffsumgt  47278  sge0gtfsumgt  47279  sge0uzfsumgt  47280  sge0seq  47282  sge0reuz  47283  omeiunltfirp  47355  carageniuncllem2  47358  caratheodorylem2  47363