Theorem sspwuni 4985

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 4502	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3133	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3903	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4832	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∀wral 3106   ⊆ wss 3881  𝒫 cpw 4497  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-pw 4499  df-uni 4801

This theorem is referenced by:  pwssb  4986  elpwpw  4987  elpwuni  4990  intss2  4993  rintn0  4994  dftr4  5141  uniixp  8468  fipwss  8877  dffi3  8879  uniwf  9232  numacn  9460  dfac12lem2  9555  fin23lem32  9755  isf34lem4  9788  isf34lem5  9789  fin1a2lem12  9822  itunitc1  9831  fpwwe2lem12  10052  tsksuc  10173  unirnioo  12827  restid  16699  mrcuni  16884  isacs3lem  17768  dmdprdd  19114  dprdfeq0  19137  dprdres  19143  dprdss  19144  dprdz  19145  subgdmdprd  19149  subgdprd  19150  dprd2dlem1  19156  dprd2da  19157  dmdprdsplit2lem  19160  ablfac1b  19185  lssintcl  19729  lbsextlem2  19924  lbsextlem3  19925  cssmre  20382  topgele  21535  topontopn  21545  unitg  21572  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  mretopd  21697  resttopon  21766  ordtuni  21795  conncompcld  22039  islocfin  22122  kgentopon  22143  txuni2  22170  ptuni2  22181  ptbasfi  22186  xkouni  22204  prdstopn  22233  txdis  22237  txcmplem2  22247  xkococnlem  22264  qtoptop2  22304  qtopuni  22307  tgqtop  22317  opnfbas  22447  neifil  22485  filunibas  22486  trfil1  22491  flimfil  22574  cldsubg  22716  tgpconncompeqg  22717  tgpconncomp  22718  tsmsxplem1  22758  utoptop  22840  unirnblps  23026  unirnbl  23027  setsmstopn  23085  tngtopn  23256  bndth  23563  bcthlem5  23932  ovolficcss  24073  ovollb  24083  voliunlem2  24155  voliunlem3  24156  uniioovol  24183  uniioombl  24193  opnmbllem  24205  ubthlem1  28653  hsupcl  29122  hsupss  29124  hsupunss  29126  hsupval2  29192  fnpreimac  30434  unicls  31256  pwsiga  31499  sigainb  31505  insiga  31506  pwldsys  31526  ddemeas  31605  omssubadd  31668  cvmsss2  32634  dfon2lem2  33142  ntruni  33788  clsint2  33790  neibastop1  33820  neibastop2lem  33821  neibastop3  33823  topmeet  33825  topjoin  33826  fnemeet1  33827  fnemeet2  33828  fnejoin1  33829  opnmbllem0  35093  heiborlem1  35249  elrfi  39635  pwpwuni  41691  0ome  43168