Theorem sspwuni 5008

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 4518	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3088	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3888	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4853	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 209   ∈ wcel 2110  ∀wral 3061   ⊆ wss 3866  𝒫 cpw 4513  ∪ cuni 4819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-11 2158  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-v 3410  df-in 3873  df-ss 3883  df-pw 4515  df-uni 4820

This theorem is referenced by:  pwssb  5009  elpwpw  5010  elpwuni  5013  intss2  5016  rintn0  5017  dftr4  5166  uniixp  8602  fipwss  9045  dffi3  9047  uniwf  9435  numacn  9663  dfac12lem2  9758  fin23lem32  9958  isf34lem4  9991  isf34lem5  9992  fin1a2lem12  10025  itunitc1  10034  fpwwe2lem11  10255  tsksuc  10376  unirnioo  13037  restid  16938  mrcuni  17124  isacs3lem  18048  dmdprdd  19386  dprdfeq0  19409  dprdres  19415  dprdss  19416  dprdz  19417  subgdmdprd  19421  subgdprd  19422  dprd2dlem1  19428  dprd2da  19429  dmdprdsplit2lem  19432  ablfac1b  19457  lssintcl  20001  lbsextlem2  20196  lbsextlem3  20197  cssmre  20655  topgele  21827  topontopn  21837  unitg  21864  fctop  21901  cctop  21903  ppttop  21904  epttop  21906  mretopd  21989  resttopon  22058  ordtuni  22087  conncompcld  22331  islocfin  22414  kgentopon  22435  txuni2  22462  ptuni2  22473  ptbasfi  22478  xkouni  22496  prdstopn  22525  txdis  22529  txcmplem2  22539  xkococnlem  22556  qtoptop2  22596  qtopuni  22599  tgqtop  22609  opnfbas  22739  neifil  22777  filunibas  22778  trfil1  22783  flimfil  22866  cldsubg  23008  tgpconncompeqg  23009  tgpconncomp  23010  tsmsxplem1  23050  utoptop  23132  unirnblps  23317  unirnbl  23318  setsmstopn  23376  tngtopn  23548  bndth  23855  bcthlem5  24225  ovolficcss  24366  ovollb  24376  voliunlem2  24448  voliunlem3  24449  uniioovol  24476  uniioombl  24486  opnmbllem  24498  ubthlem1  28951  hsupcl  29420  hsupss  29422  hsupunss  29424  hsupval2  29490  fnpreimac  30728  unicls  31567  pwsiga  31810  sigainb  31816  insiga  31817  pwldsys  31837  ddemeas  31916  omssubadd  31979  cvmsss2  32949  dfon2lem2  33479  ntruni  34253  clsint2  34255  neibastop1  34285  neibastop2lem  34286  neibastop3  34288  topmeet  34290  topjoin  34291  fnemeet1  34292  fnemeet2  34293  fnejoin1  34294  opnmbllem0  35550  heiborlem1  35706  elrfi  40219  pwpwuni  42278  0ome  43742