Theorem sspwuni 5065

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.

Step	Hyp	Ref	Expression
1		velpw 4570	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3935	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4905	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2106  ∀wral 3060   ⊆ wss 3913  𝒫 cpw 4565  ∪ cuni 4870

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-in 3920  df-ss 3930  df-pw 4567  df-uni 4871

This theorem is referenced by:  pwssb  5066  elpwpw  5067  elpwuni  5070  intss2  5073  rintn0  5074  dftr4  5234  uniixp  8866  fipwss  9374  dffi3  9376  uniwf  9764  numacn  9994  dfac12lem2  10089  fin23lem32  10289  isf34lem4  10322  isf34lem5  10323  fin1a2lem12  10356  itunitc1  10365  fpwwe2lem11  10586  tsksuc  10707  unirnioo  13376  restid  17329  mrcuni  17515  isacs3lem  18445  dmdprdd  19792  dprdfeq0  19815  dprdres  19821  dprdss  19822  dprdz  19823  subgdmdprd  19827  subgdprd  19828  dprd2dlem1  19834  dprd2da  19835  dmdprdsplit2lem  19838  ablfac1b  19863  lssintcl  20482  lbsextlem2  20679  lbsextlem3  20680  cssmre  21134  topgele  22316  topontopn  22326  unitg  22354  fctop  22391  cctop  22393  ppttop  22394  epttop  22396  mretopd  22480  resttopon  22549  ordtuni  22578  conncompcld  22822  islocfin  22905  kgentopon  22926  txuni2  22953  ptuni2  22964  ptbasfi  22969  xkouni  22987  prdstopn  23016  txdis  23020  txcmplem2  23030  xkococnlem  23047  qtoptop2  23087  qtopuni  23090  tgqtop  23100  opnfbas  23230  neifil  23268  filunibas  23269  trfil1  23274  flimfil  23357  cldsubg  23499  tgpconncompeqg  23500  tgpconncomp  23501  tsmsxplem1  23541  utoptop  23623  unirnblps  23809  unirnbl  23810  setsmstopn  23870  tngtopn  24051  bndth  24358  bcthlem5  24729  ovolficcss  24870  ovollb  24880  voliunlem2  24952  voliunlem3  24953  uniioovol  24980  uniioombl  24990  opnmbllem  25002  ubthlem1  29875  hsupcl  30344  hsupss  30346  hsupunss  30348  hsupval2  30414  fnpreimac  31654  unicls  32573  pwsiga  32818  sigainb  32824  insiga  32825  pwldsys  32845  ddemeas  32924  omssubadd  32989  cvmsss2  33955  dfon2lem2  34445  ntruni  34875  clsint2  34877  neibastop1  34907  neibastop2lem  34908  neibastop3  34910  topmeet  34912  topjoin  34913  fnemeet1  34914  fnemeet2  34915  fnejoin1  34916  opnmbllem0  36187  heiborlem1  36343  elrfi  41075  pwpwuni  43387  0ome  44890