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

Theorem sspwuni 3973
Description: Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
Assertion
Ref Expression
sspwuni (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)

Proof of Theorem sspwuni
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 vex 2742 . . . 4 𝑥 ∈ V
21elpw 3583 . . 3 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
32ralbii 2483 . 2 (∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
4 dfss3 3147 . 2 (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵)
5 unissb 3841 . 2 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
63, 4, 53bitr4i 212 1 (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wb 105  wcel 2148  wral 2455  wss 3131  𝒫 cpw 3577   cuni 3811
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-ral 2460  df-v 2741  df-in 3137  df-ss 3144  df-pw 3579  df-uni 3812
This theorem is referenced by:  pwssb  3974  elpwpw  3975  elpwuni  3978  rintm  3981  dftr4  4108  iotass  5197  tfrlemibfn  6331  tfr1onlembfn  6347  tfrcllembfn  6360  uniixp  6723  fipwssg  6980  unirnioo  9975  restid  12704  lssintclm  13476  topgele  13568  topontopn  13576  unitg  13601  epttop  13629  resttopon  13710  txuni2  13795  txdis  13816  unirnblps  13961  unirnbl  13962
  Copyright terms: Public domain W3C validator