Theorem sspwuni 5107

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 4611	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3082	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3967	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4946	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 205   ∈ wcel 2098  ∀wral 3050   ⊆ wss 3946  𝒫 cpw 4606  ∪ cuni 4912

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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-v 3463  df-ss 3963  df-pw 4608  df-uni 4913

This theorem is referenced by:  pwssb  5108  elpwpw  5109  elpwuni  5112  intss2  5115  rintn0  5116  dftr4  5276  uniixp  8949  fipwss  9468  dffi3  9470  uniwf  9858  numacn  10088  dfac12lem2  10183  fin23lem32  10383  isf34lem4  10416  isf34lem5  10417  fin1a2lem12  10450  itunitc1  10459  fpwwe2lem11  10680  tsksuc  10801  unirnioo  13475  restid  17443  mrcuni  17629  isacs3lem  18562  dmdprdd  19994  dprdfeq0  20017  dprdres  20023  dprdss  20024  dprdz  20025  subgdmdprd  20029  subgdprd  20030  dprd2dlem1  20036  dprd2da  20037  dmdprdsplit2lem  20040  ablfac1b  20065  lssintcl  20888  lbsextlem2  21087  lbsextlem3  21088  cssmre  21681  topgele  22915  topontopn  22925  unitg  22953  fctop  22990  cctop  22992  ppttop  22993  epttop  22995  mretopd  23079  resttopon  23148  ordtuni  23177  conncompcld  23421  islocfin  23504  kgentopon  23525  txuni2  23552  ptuni2  23563  ptbasfi  23568  xkouni  23586  prdstopn  23615  txdis  23619  txcmplem2  23629  xkococnlem  23646  qtoptop2  23686  qtopuni  23689  tgqtop  23699  opnfbas  23829  neifil  23867  filunibas  23868  trfil1  23873  flimfil  23956  cldsubg  24098  tgpconncompeqg  24099  tgpconncomp  24100  tsmsxplem1  24140  utoptop  24222  unirnblps  24408  unirnbl  24409  setsmstopn  24469  tngtopn  24650  bndth  24967  bcthlem5  25339  ovolficcss  25481  ovollb  25491  voliunlem2  25563  voliunlem3  25564  uniioovol  25591  uniioombl  25601  opnmbllem  25613  ubthlem1  30795  hsupcl  31264  hsupss  31266  hsupunss  31268  hsupval2  31334  fnpreimac  32579  unicls  33674  pwsiga  33919  sigainb  33925  insiga  33926  pwldsys  33946  ddemeas  34025  omssubadd  34090  cvmsss2  35054  dfon2lem2  35556  ntruni  35987  clsint2  35989  neibastop1  36019  neibastop2lem  36020  neibastop3  36022  topmeet  36024  topjoin  36025  fnemeet1  36026  fnemeet2  36027  fnejoin1  36028  opnmbllem0  37305  heiborlem1  37460  elrfi  42288  pwpwuni  44595  0ome  46087