Theorem sspwuni 5033

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

Syntax hints:   ↔ wb 205   ∈ wcel 2109  ∀wral 3065   ⊆ wss 3891  𝒫 cpw 4538  ∪ cuni 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-11 2157  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-v 3432  df-in 3898  df-ss 3908  df-pw 4540  df-uni 4845

This theorem is referenced by:  pwssb  5034  elpwpw  5035  elpwuni  5038  intss2  5041  rintn0  5042  dftr4  5200  uniixp  8683  fipwss  9149  dffi3  9151  uniwf  9561  numacn  9789  dfac12lem2  9884  fin23lem32  10084  isf34lem4  10117  isf34lem5  10118  fin1a2lem12  10151  itunitc1  10160  fpwwe2lem11  10381  tsksuc  10502  unirnioo  13163  restid  17125  mrcuni  17311  isacs3lem  18241  dmdprdd  19583  dprdfeq0  19606  dprdres  19612  dprdss  19613  dprdz  19614  subgdmdprd  19618  subgdprd  19619  dprd2dlem1  19625  dprd2da  19626  dmdprdsplit2lem  19629  ablfac1b  19654  lssintcl  20207  lbsextlem2  20402  lbsextlem3  20403  cssmre  20879  topgele  22060  topontopn  22070  unitg  22098  fctop  22135  cctop  22137  ppttop  22138  epttop  22140  mretopd  22224  resttopon  22293  ordtuni  22322  conncompcld  22566  islocfin  22649  kgentopon  22670  txuni2  22697  ptuni2  22708  ptbasfi  22713  xkouni  22731  prdstopn  22760  txdis  22764  txcmplem2  22774  xkococnlem  22791  qtoptop2  22831  qtopuni  22834  tgqtop  22844  opnfbas  22974  neifil  23012  filunibas  23013  trfil1  23018  flimfil  23101  cldsubg  23243  tgpconncompeqg  23244  tgpconncomp  23245  tsmsxplem1  23285  utoptop  23367  unirnblps  23553  unirnbl  23554  setsmstopn  23614  tngtopn  23795  bndth  24102  bcthlem5  24473  ovolficcss  24614  ovollb  24624  voliunlem2  24696  voliunlem3  24697  uniioovol  24724  uniioombl  24734  opnmbllem  24746  ubthlem1  29211  hsupcl  29680  hsupss  29682  hsupunss  29684  hsupval2  29750  fnpreimac  30987  unicls  31832  pwsiga  32077  sigainb  32083  insiga  32084  pwldsys  32104  ddemeas  32183  omssubadd  32246  cvmsss2  33215  dfon2lem2  33739  ntruni  34495  clsint2  34497  neibastop1  34527  neibastop2lem  34528  neibastop3  34530  topmeet  34532  topjoin  34533  fnemeet1  34534  fnemeet2  34535  fnejoin1  34536  opnmbllem0  35792  heiborlem1  35948  elrfi  40496  pwpwuni  42558  0ome  44021