Theorem sselpwd 4734

Description: Elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020.)

Hypotheses

Ref	Expression
sselpwd.1	⊢ (𝜑 → 𝐵 ∈ 𝑉)
sselpwd.2	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sselpwd	⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Proof of Theorem sselpwd

Step	Hyp	Ref	Expression
1		sselpwd.2	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sselpwd.1	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
3	2, 1	ssexd 4733	. . 3 ⊢ (𝜑 → 𝐴 ∈ V)
4		elpwg 4116	. . 3 ⊢ (𝐴 ∈ V → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
5	3, 4	syl 17	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵))
6	1, 5	mpbird 246	1 ⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110

This theorem is referenced by:  fin1a2lem7  9111  ustssel  21819  ldsysgenld  29550  ldgenpisyslem1  29553  rfovcnvf1od  37318  fsovrfovd  37323  fsovfd  37326  fsovcnvlem  37327  ntrclsrcomplex  37353  clsk3nimkb  37358  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  ntrclsiso  37385  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrneircomplex  37392  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  clsneircomplex  37421  clsneiel1  37426  neicvgrcomplex  37431  neicvgel1  37437  ovolsplit  38881