Theorem sspwuni 5105

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 4610	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3984	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4944	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2106  ∀wral 3059   ⊆ wss 3963  𝒫 cpw 4605  ∪ cuni 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-v 3480  df-ss 3980  df-pw 4607  df-uni 4913

This theorem is referenced by:  pwssb  5106  elpwpw  5107  elpwuni  5110  intss2  5113  rintn0  5114  dftr4  5272  uniixp  8960  fipwss  9467  dffi3  9469  uniwf  9857  numacn  10087  dfac12lem2  10183  fin23lem32  10382  isf34lem4  10415  isf34lem5  10416  fin1a2lem12  10449  itunitc1  10458  fpwwe2lem11  10679  tsksuc  10800  unirnioo  13486  restid  17480  mrcuni  17666  isacs3lem  18600  dmdprdd  20034  dprdfeq0  20057  dprdres  20063  dprdss  20064  dprdz  20065  subgdmdprd  20069  subgdprd  20070  dprd2dlem1  20076  dprd2da  20077  dmdprdsplit2lem  20080  ablfac1b  20105  lssintcl  20980  lbsextlem2  21179  lbsextlem3  21180  cssmre  21729  topgele  22952  topontopn  22962  unitg  22990  fctop  23027  cctop  23029  ppttop  23030  epttop  23032  mretopd  23116  resttopon  23185  ordtuni  23214  conncompcld  23458  islocfin  23541  kgentopon  23562  txuni2  23589  ptuni2  23600  ptbasfi  23605  xkouni  23623  prdstopn  23652  txdis  23656  txcmplem2  23666  xkococnlem  23683  qtoptop2  23723  qtopuni  23726  tgqtop  23736  opnfbas  23866  neifil  23904  filunibas  23905  trfil1  23910  flimfil  23993  cldsubg  24135  tgpconncompeqg  24136  tgpconncomp  24137  tsmsxplem1  24177  utoptop  24259  unirnblps  24445  unirnbl  24446  setsmstopn  24506  tngtopn  24687  bndth  25004  bcthlem5  25376  ovolficcss  25518  ovollb  25528  voliunlem2  25600  voliunlem3  25601  uniioovol  25628  uniioombl  25638  opnmbllem  25650  ubthlem1  30899  hsupcl  31368  hsupss  31370  hsupunss  31372  hsupval2  31438  fnpreimac  32688  unicls  33864  pwsiga  34111  sigainb  34117  insiga  34118  pwldsys  34138  ddemeas  34217  omssubadd  34282  cvmsss2  35259  dfon2lem2  35766  ntruni  36310  clsint2  36312  neibastop1  36342  neibastop2lem  36343  neibastop3  36345  topmeet  36347  topjoin  36348  fnemeet1  36349  fnemeet2  36350  fnejoin1  36351  opnmbllem0  37643  heiborlem1  37798  elrfi  42682  pwpwuni  44997  0ome  46485