Theorem sspwuni 5067

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3045   ⊆ wss 3917  𝒫 cpw 4566  ∪ cuni 4874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-v 3452  df-ss 3934  df-pw 4568  df-uni 4875

This theorem is referenced by:  pwssb  5068  elpwpw  5069  elpwuni  5072  intss2  5075  rintn0  5076  dftr4  5224  uniixp  8897  fipwss  9387  dffi3  9389  uniwf  9779  numacn  10009  dfac12lem2  10105  fin23lem32  10304  isf34lem4  10337  isf34lem5  10338  fin1a2lem12  10371  itunitc1  10380  fpwwe2lem11  10601  tsksuc  10722  unirnioo  13417  restid  17403  mrcuni  17589  isacs3lem  18508  dmdprdd  19938  dprdfeq0  19961  dprdres  19967  dprdss  19968  dprdz  19969  subgdmdprd  19973  subgdprd  19974  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  ablfac1b  20009  lssintcl  20877  lbsextlem2  21076  lbsextlem3  21077  cssmre  21609  topgele  22824  topontopn  22834  unitg  22861  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  mretopd  22986  resttopon  23055  ordtuni  23084  conncompcld  23328  islocfin  23411  kgentopon  23432  txuni2  23459  ptuni2  23470  ptbasfi  23475  xkouni  23493  prdstopn  23522  txdis  23526  txcmplem2  23536  xkococnlem  23553  qtoptop2  23593  qtopuni  23596  tgqtop  23606  opnfbas  23736  neifil  23774  filunibas  23775  trfil1  23780  flimfil  23863  cldsubg  24005  tgpconncompeqg  24006  tgpconncomp  24007  tsmsxplem1  24047  utoptop  24129  unirnblps  24314  unirnbl  24315  setsmstopn  24373  tngtopn  24545  bndth  24864  bcthlem5  25235  ovolficcss  25377  ovollb  25387  voliunlem2  25459  voliunlem3  25460  uniioovol  25487  uniioombl  25497  opnmbllem  25509  ubthlem1  30806  hsupcl  31275  hsupss  31277  hsupunss  31279  hsupval2  31345  fnpreimac  32602  unicls  33900  pwsiga  34127  sigainb  34133  insiga  34134  pwldsys  34154  ddemeas  34233  omssubadd  34298  cvmsss2  35268  dfon2lem2  35779  ntruni  36322  clsint2  36324  neibastop1  36354  neibastop2lem  36355  neibastop3  36357  topmeet  36359  topjoin  36360  fnemeet1  36361  fnemeet2  36362  fnejoin1  36363  opnmbllem0  37657  heiborlem1  37812  elrfi  42689  pwpwuni  45058  0ome  46534