Theorem sspwuni 5048

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  ∀wral 3047   ⊆ wss 3902  𝒫 cpw 4550  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-v 3438  df-ss 3919  df-pw 4552  df-uni 4860

This theorem is referenced by:  pwssb  5049  elpwpw  5050  elpwuni  5053  intss2  5056  rintn0  5057  dftr4  5204  uniixp  8845  fipwss  9313  dffi3  9315  uniwf  9709  numacn  9937  dfac12lem2  10033  fin23lem32  10232  isf34lem4  10265  isf34lem5  10266  fin1a2lem12  10299  itunitc1  10308  fpwwe2lem11  10529  tsksuc  10650  unirnioo  13346  restid  17334  mrcuni  17524  isacs3lem  18445  dmdprdd  19911  dprdfeq0  19934  dprdres  19940  dprdss  19941  dprdz  19942  subgdmdprd  19946  subgdprd  19947  dprd2dlem1  19953  dprd2da  19954  dmdprdsplit2lem  19957  ablfac1b  19982  lssintcl  20895  lbsextlem2  21094  lbsextlem3  21095  cssmre  21628  topgele  22843  topontopn  22853  unitg  22880  fctop  22917  cctop  22919  ppttop  22920  epttop  22922  mretopd  23005  resttopon  23074  ordtuni  23103  conncompcld  23347  islocfin  23430  kgentopon  23451  txuni2  23478  ptuni2  23489  ptbasfi  23494  xkouni  23512  prdstopn  23541  txdis  23545  txcmplem2  23555  xkococnlem  23572  qtoptop2  23612  qtopuni  23615  tgqtop  23625  opnfbas  23755  neifil  23793  filunibas  23794  trfil1  23799  flimfil  23882  cldsubg  24024  tgpconncompeqg  24025  tgpconncomp  24026  tsmsxplem1  24066  utoptop  24147  unirnblps  24332  unirnbl  24333  setsmstopn  24391  tngtopn  24563  bndth  24882  bcthlem5  25253  ovolficcss  25395  ovollb  25405  voliunlem2  25477  voliunlem3  25478  uniioovol  25505  uniioombl  25515  opnmbllem  25527  ubthlem1  30845  hsupcl  31314  hsupss  31316  hsupunss  31318  hsupval2  31384  fnpreimac  32648  unicls  33911  pwsiga  34138  sigainb  34144  insiga  34145  pwldsys  34165  ddemeas  34244  omssubadd  34308  cvmsss2  35306  dfon2lem2  35817  ntruni  36360  clsint2  36362  neibastop1  36392  neibastop2lem  36393  neibastop3  36395  topmeet  36397  topjoin  36398  fnemeet1  36399  fnemeet2  36400  fnejoin1  36401  opnmbllem0  37695  heiborlem1  37850  elrfi  42726  pwpwuni  45093  0ome  46566