ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elpwid GIF version

Theorem elpwid 3585
Description: An element of a power class is a subclass. Deduction form of elpwi 3583. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
elpwid.1 (𝜑𝐴 ∈ 𝒫 𝐵)
Assertion
Ref Expression
elpwid (𝜑𝐴𝐵)

Proof of Theorem elpwid
StepHypRef Expression
1 elpwid.1 . 2 (𝜑𝐴 ∈ 𝒫 𝐵)
2 elpwi 3583 . 2 (𝐴 ∈ 𝒫 𝐵𝐴𝐵)
31, 2syl 14 1 (𝜑𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wss 3129  𝒫 cpw 3574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-in 3135  df-ss 3142  df-pw 3576
This theorem is referenced by:  fopwdom  6830  ssenen  6845  fival  6963  fiuni  6971  3nelsucpw1  7227  elnp1st2nd  7466  ixxssxr  9887  elfzoelz  10133  restid2  12645  epttop  13257  neiss2  13309  blssm  13588  blin2  13599  cncfrss  13729  cncfrss2  13730  pwle2  14404
  Copyright terms: Public domain W3C validator