Theorem sspwuni 5076

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∀wral 3051   ⊆ wss 3926  𝒫 cpw 4575  ∪ cuni 4883

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-v 3461  df-ss 3943  df-pw 4577  df-uni 4884

This theorem is referenced by:  pwssb  5077  elpwpw  5078  elpwuni  5081  intss2  5084  rintn0  5085  dftr4  5236  uniixp  8935  fipwss  9441  dffi3  9443  uniwf  9833  numacn  10063  dfac12lem2  10159  fin23lem32  10358  isf34lem4  10391  isf34lem5  10392  fin1a2lem12  10425  itunitc1  10434  fpwwe2lem11  10655  tsksuc  10776  unirnioo  13466  restid  17447  mrcuni  17633  isacs3lem  18552  dmdprdd  19982  dprdfeq0  20005  dprdres  20011  dprdss  20012  dprdz  20013  subgdmdprd  20017  subgdprd  20018  dprd2dlem1  20024  dprd2da  20025  dmdprdsplit2lem  20028  ablfac1b  20053  lssintcl  20921  lbsextlem2  21120  lbsextlem3  21121  cssmre  21653  topgele  22868  topontopn  22878  unitg  22905  fctop  22942  cctop  22944  ppttop  22945  epttop  22947  mretopd  23030  resttopon  23099  ordtuni  23128  conncompcld  23372  islocfin  23455  kgentopon  23476  txuni2  23503  ptuni2  23514  ptbasfi  23519  xkouni  23537  prdstopn  23566  txdis  23570  txcmplem2  23580  xkococnlem  23597  qtoptop2  23637  qtopuni  23640  tgqtop  23650  opnfbas  23780  neifil  23818  filunibas  23819  trfil1  23824  flimfil  23907  cldsubg  24049  tgpconncompeqg  24050  tgpconncomp  24051  tsmsxplem1  24091  utoptop  24173  unirnblps  24358  unirnbl  24359  setsmstopn  24417  tngtopn  24589  bndth  24908  bcthlem5  25280  ovolficcss  25422  ovollb  25432  voliunlem2  25504  voliunlem3  25505  uniioovol  25532  uniioombl  25542  opnmbllem  25554  ubthlem1  30851  hsupcl  31320  hsupss  31322  hsupunss  31324  hsupval2  31390  fnpreimac  32649  unicls  33934  pwsiga  34161  sigainb  34167  insiga  34168  pwldsys  34188  ddemeas  34267  omssubadd  34332  cvmsss2  35296  dfon2lem2  35802  ntruni  36345  clsint2  36347  neibastop1  36377  neibastop2lem  36378  neibastop3  36380  topmeet  36382  topjoin  36383  fnemeet1  36384  fnemeet2  36385  fnejoin1  36386  opnmbllem0  37680  heiborlem1  37835  elrfi  42717  pwpwuni  45081  0ome  46558