Theorem sspwuni 5104

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  ∀wral 3062   ⊆ wss 3949  𝒫 cpw 4603  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-pw 4605  df-uni 4910

This theorem is referenced by:  pwssb  5105  elpwpw  5106  elpwuni  5109  intss2  5112  rintn0  5113  dftr4  5273  uniixp  8915  fipwss  9424  dffi3  9426  uniwf  9814  numacn  10044  dfac12lem2  10139  fin23lem32  10339  isf34lem4  10372  isf34lem5  10373  fin1a2lem12  10406  itunitc1  10415  fpwwe2lem11  10636  tsksuc  10757  unirnioo  13426  restid  17379  mrcuni  17565  isacs3lem  18495  dmdprdd  19869  dprdfeq0  19892  dprdres  19898  dprdss  19899  dprdz  19900  subgdmdprd  19904  subgdprd  19905  dprd2dlem1  19911  dprd2da  19912  dmdprdsplit2lem  19915  ablfac1b  19940  lssintcl  20575  lbsextlem2  20772  lbsextlem3  20773  cssmre  21246  topgele  22432  topontopn  22442  unitg  22470  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  mretopd  22596  resttopon  22665  ordtuni  22694  conncompcld  22938  islocfin  23021  kgentopon  23042  txuni2  23069  ptuni2  23080  ptbasfi  23085  xkouni  23103  prdstopn  23132  txdis  23136  txcmplem2  23146  xkococnlem  23163  qtoptop2  23203  qtopuni  23206  tgqtop  23216  opnfbas  23346  neifil  23384  filunibas  23385  trfil1  23390  flimfil  23473  cldsubg  23615  tgpconncompeqg  23616  tgpconncomp  23617  tsmsxplem1  23657  utoptop  23739  unirnblps  23925  unirnbl  23926  setsmstopn  23986  tngtopn  24167  bndth  24474  bcthlem5  24845  ovolficcss  24986  ovollb  24996  voliunlem2  25068  voliunlem3  25069  uniioovol  25096  uniioombl  25106  opnmbllem  25118  ubthlem1  30123  hsupcl  30592  hsupss  30594  hsupunss  30596  hsupval2  30662  fnpreimac  31896  unicls  32883  pwsiga  33128  sigainb  33134  insiga  33135  pwldsys  33155  ddemeas  33234  omssubadd  33299  cvmsss2  34265  dfon2lem2  34756  ntruni  35212  clsint2  35214  neibastop1  35244  neibastop2lem  35245  neibastop3  35247  topmeet  35249  topjoin  35250  fnemeet1  35251  fnemeet2  35252  fnejoin1  35253  opnmbllem0  36524  heiborlem1  36679  elrfi  41432  pwpwuni  43744  0ome  45245