MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspwuni Structured version   Visualization version   GIF version

Theorem sspwuni 5014
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 velpw 4545 . . 3 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
21ralbii 3165 . 2 (∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
3 dfss3 3955 . 2 (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵)
4 unissb 4863 . 2 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
52, 3, 43bitr4i 304 1 (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2105  wral 3138  wss 3935  𝒫 cpw 4537   cuni 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3497  df-in 3942  df-ss 3951  df-pw 4539  df-uni 4833
This theorem is referenced by:  pwssb  5015  elpwpw  5016  elpwuni  5019  rintn0  5022  dftr4  5169  uniixp  8474  fipwss  8882  dffi3  8884  uniwf  9237  numacn  9464  dfac12lem2  9559  fin23lem32  9755  isf34lem4  9788  isf34lem5  9789  fin1a2lem12  9822  itunitc1  9831  fpwwe2lem12  10052  tsksuc  10173  unirnioo  12827  restid  16697  mrcuni  16882  isacs3lem  17766  dmdprdd  19052  dprdfeq0  19075  dprdres  19081  dprdss  19082  dprdz  19083  subgdmdprd  19087  subgdprd  19088  dprd2dlem1  19094  dprd2da  19095  dmdprdsplit2lem  19098  ablfac1b  19123  lssintcl  19667  lbsextlem2  19862  lbsextlem3  19863  cssmre  20767  topgele  21468  topontopn  21478  unitg  21505  fctop  21542  cctop  21544  ppttop  21545  epttop  21547  mretopd  21630  resttopon  21699  ordtuni  21728  conncompcld  21972  islocfin  22055  kgentopon  22076  txuni2  22103  ptuni2  22114  ptbasfi  22119  xkouni  22137  prdstopn  22166  txdis  22170  txcmplem2  22180  xkococnlem  22197  qtoptop2  22237  qtopuni  22240  tgqtop  22250  opnfbas  22380  neifil  22418  filunibas  22419  trfil1  22424  flimfil  22507  cldsubg  22648  tgpconncompeqg  22649  tgpconncomp  22650  tsmsxplem1  22690  utoptop  22772  unirnblps  22958  unirnbl  22959  setsmstopn  23017  tngtopn  23188  bndth  23491  bcthlem5  23860  ovolficcss  23999  ovollb  24009  voliunlem2  24081  voliunlem3  24082  uniioovol  24109  uniioombl  24119  opnmbllem  24131  ubthlem1  28575  hsupcl  29044  hsupss  29046  hsupunss  29048  hsupval2  29114  fnpreimac  30345  unicls  31046  pwsiga  31289  sigainb  31295  insiga  31296  ddemeas  31395  omssubadd  31458  cvmsss2  32419  dfon2lem2  32927  ntruni  33573  clsint2  33575  neibastop1  33605  neibastop2lem  33606  neibastop3  33608  topmeet  33610  topjoin  33611  fnemeet1  33612  fnemeet2  33613  fnejoin1  33614  bj-intss  34286  opnmbllem0  34810  heiborlem1  34972  elrfi  39171  pwpwuni  41199  0ome  42692
  Copyright terms: Public domain W3C validator