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

Theorem sspwuni 5018
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 4549 . . 3 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
21ralbii 3169 . 2 (∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
3 dfss3 3959 . 2 (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥𝐴 𝑥 ∈ 𝒫 𝐵)
4 unissb 4867 . 2 ( 𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
52, 3, 43bitr4i 304 1 (𝐴 ⊆ 𝒫 𝐵 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wcel 2107  wral 3142  wss 3939  𝒫 cpw 4541   cuni 4836
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ral 3147  df-v 3501  df-in 3946  df-ss 3955  df-pw 4543  df-uni 4837
This theorem is referenced by:  pwssb  5019  elpwpw  5020  elpwuni  5023  rintn0  5026  dftr4  5173  uniixp  8477  fipwss  8885  dffi3  8887  uniwf  9240  numacn  9467  dfac12lem2  9562  fin23lem32  9758  isf34lem4  9791  isf34lem5  9792  fin1a2lem12  9825  itunitc1  9834  fpwwe2lem12  10055  tsksuc  10176  unirnioo  12830  restid  16699  mrcuni  16884  isacs3lem  17768  dmdprdd  19043  dprdfeq0  19066  dprdres  19072  dprdss  19073  dprdz  19074  subgdmdprd  19078  subgdprd  19079  dprd2dlem1  19085  dprd2da  19086  dmdprdsplit2lem  19089  ablfac1b  19114  lssintcl  19658  lbsextlem2  19853  lbsextlem3  19854  cssmre  20755  topgele  21456  topontopn  21466  unitg  21493  fctop  21530  cctop  21532  ppttop  21533  epttop  21535  mretopd  21618  resttopon  21687  ordtuni  21716  conncompcld  21960  islocfin  22043  kgentopon  22064  txuni2  22091  ptuni2  22102  ptbasfi  22107  xkouni  22125  prdstopn  22154  txdis  22158  txcmplem2  22168  xkococnlem  22185  qtoptop2  22225  qtopuni  22228  tgqtop  22238  opnfbas  22368  neifil  22406  filunibas  22407  trfil1  22412  flimfil  22495  cldsubg  22636  tgpconncompeqg  22637  tgpconncomp  22638  tsmsxplem1  22678  utoptop  22760  unirnblps  22946  unirnbl  22947  setsmstopn  23005  tngtopn  23176  bndth  23479  bcthlem5  23848  ovolficcss  23987  ovollb  23997  voliunlem2  24069  voliunlem3  24070  uniioovol  24097  uniioombl  24107  opnmbllem  24119  ubthlem1  28563  hsupcl  29032  hsupss  29034  hsupunss  29036  hsupval2  29102  fnpreimac  30333  unicls  31034  pwsiga  31277  sigainb  31283  insiga  31284  ddemeas  31383  omssubadd  31446  cvmsss2  32407  dfon2lem2  32915  ntruni  33561  clsint2  33563  neibastop1  33593  neibastop2lem  33594  neibastop3  33596  topmeet  33598  topjoin  33599  fnemeet1  33600  fnemeet2  33601  fnejoin1  33602  bj-intss  34274  opnmbllem0  34797  heiborlem1  34959  elrfi  39158  pwpwuni  41186  0ome  42679
  Copyright terms: Public domain W3C validator