Theorem sspwuni 5056

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 4559	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3107	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3925	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4898	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 208   ∈ wcel 2141  ∀wral 3075   ⊆ wss 3904  𝒫 cpw 4554  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-v 3455  df-ss 3921  df-pw 4556  df-uni 4865

This theorem is referenced by:  pwssb  5057  elpwpw  5058  elpwuni  5061  intss2  5064  rintn0  5065  dftr4  5212  uniixp  8899  fipwss  9372  dffi3  9374  uniwf  9774  numacn  10002  dfac12lem2  10098  fin23lem32  10298  isf34lem4  10331  isf34lem5  10332  fin1a2lem12  10365  itunitc1  10374  fpwwe2lem11  10596  tsksuc  10717  unirnioo  13450  restid  17445  mrcuni  17636  isacs3lem  18557  dmdprdd  20024  dprdfeq0  20047  dprdres  20053  dprdss  20054  dprdz  20055  subgdmdprd  20059  subgdprd  20060  dprd2dlem1  20066  dprd2da  20067  dmdprdsplit2lem  20070  ablfac1b  20095  lssintcl  21011  lbsextlem2  21209  lbsextlem3  21210  cssmre  21725  topgele  22970  topontopn  22980  unitg  23007  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  mretopd  23132  resttopon  23201  ordtuni  23230  conncompcld  23474  islocfin  23557  kgentopon  23578  txuni2  23605  ptuni2  23616  ptbasfi  23621  xkouni  23639  prdstopn  23668  txdis  23672  txcmplem2  23682  xkococnlem  23699  qtoptop2  23739  qtopuni  23742  tgqtop  23752  opnfbas  23882  neifil  23920  filunibas  23921  trfil1  23926  flimfil  24009  cldsubg  24151  tgpconncompeqg  24152  tgpconncomp  24153  tsmsxplem1  24193  utoptop  24274  unirnblps  24459  unirnbl  24460  setsmstopn  24518  tngtopn  24690  bndth  25000  bcthlem5  25370  ovolficcss  25511  ovollb  25521  voliunlem2  25593  voliunlem3  25594  uniioovol  25621  uniioombl  25631  opnmbllem  25643  ubthlem1  31019  hsupcl  31488  hsupss  31490  hsupunss  31492  hsupval2  31558  fnpreimac  32822  unicls  34161  pwsiga  34388  sigainb  34394  insiga  34395  pwldsys  34415  ddemeas  34494  omssubadd  34558  cvmsss2  35588  dfon2lem2  36096  ntruni  36651  clsint2  36653  neibastop1  36683  neibastop2lem  36684  neibastop3  36686  topmeet  36688  topjoin  36689  fnemeet1  36690  fnemeet2  36691  fnejoin1  36692  opnmbllem0  38119  heiborlem1  38274  elrfi  43239  pwpwuni  45601  0ome  47067