Theorem sspwuni 5055

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∀wral 3051   ⊆ wss 3901  𝒫 cpw 4554  ∪ cuni 4863

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3442  df-ss 3918  df-pw 4556  df-uni 4864

This theorem is referenced by:  pwssb  5056  elpwpw  5057  elpwuni  5060  intss2  5063  rintn0  5064  dftr4  5211  uniixp  8859  fipwss  9332  dffi3  9334  uniwf  9731  numacn  9959  dfac12lem2  10055  fin23lem32  10254  isf34lem4  10287  isf34lem5  10288  fin1a2lem12  10321  itunitc1  10330  fpwwe2lem11  10552  tsksuc  10673  unirnioo  13365  restid  17353  mrcuni  17544  isacs3lem  18465  dmdprdd  19930  dprdfeq0  19953  dprdres  19959  dprdss  19960  dprdz  19961  subgdmdprd  19965  subgdprd  19966  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  ablfac1b  20001  lssintcl  20915  lbsextlem2  21114  lbsextlem3  21115  cssmre  21648  topgele  22874  topontopn  22884  unitg  22911  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  mretopd  23036  resttopon  23105  ordtuni  23134  conncompcld  23378  islocfin  23461  kgentopon  23482  txuni2  23509  ptuni2  23520  ptbasfi  23525  xkouni  23543  prdstopn  23572  txdis  23576  txcmplem2  23586  xkococnlem  23603  qtoptop2  23643  qtopuni  23646  tgqtop  23656  opnfbas  23786  neifil  23824  filunibas  23825  trfil1  23830  flimfil  23913  cldsubg  24055  tgpconncompeqg  24056  tgpconncomp  24057  tsmsxplem1  24097  utoptop  24178  unirnblps  24363  unirnbl  24364  setsmstopn  24422  tngtopn  24594  bndth  24913  bcthlem5  25284  ovolficcss  25426  ovollb  25436  voliunlem2  25508  voliunlem3  25509  uniioovol  25536  uniioombl  25546  opnmbllem  25558  ubthlem1  30945  hsupcl  31414  hsupss  31416  hsupunss  31418  hsupval2  31484  fnpreimac  32749  unicls  34060  pwsiga  34287  sigainb  34293  insiga  34294  pwldsys  34314  ddemeas  34393  omssubadd  34457  cvmsss2  35468  dfon2lem2  35976  ntruni  36521  clsint2  36523  neibastop1  36553  neibastop2lem  36554  neibastop3  36556  topmeet  36558  topjoin  36559  fnemeet1  36560  fnemeet2  36561  fnejoin1  36562  opnmbllem0  37853  heiborlem1  38008  elrfi  42932  pwpwuni  45298  0ome  46769