Theorem sspwuni 5057

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3903  𝒫 cpw 4556  ∪ cuni 4865

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-ss 3920  df-pw 4558  df-uni 4866

This theorem is referenced by:  pwssb  5058  elpwpw  5059  elpwuni  5062  intss2  5065  rintn0  5066  dftr4  5213  uniixp  8871  fipwss  9344  dffi3  9346  uniwf  9743  numacn  9971  dfac12lem2  10067  fin23lem32  10266  isf34lem4  10299  isf34lem5  10300  fin1a2lem12  10333  itunitc1  10342  fpwwe2lem11  10564  tsksuc  10685  unirnioo  13377  restid  17365  mrcuni  17556  isacs3lem  18477  dmdprdd  19942  dprdfeq0  19965  dprdres  19971  dprdss  19972  dprdz  19973  subgdmdprd  19977  subgdprd  19978  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  ablfac1b  20013  lssintcl  20927  lbsextlem2  21126  lbsextlem3  21127  cssmre  21660  topgele  22886  topontopn  22896  unitg  22923  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  mretopd  23048  resttopon  23117  ordtuni  23146  conncompcld  23390  islocfin  23473  kgentopon  23494  txuni2  23521  ptuni2  23532  ptbasfi  23537  xkouni  23555  prdstopn  23584  txdis  23588  txcmplem2  23598  xkococnlem  23615  qtoptop2  23655  qtopuni  23658  tgqtop  23668  opnfbas  23798  neifil  23836  filunibas  23837  trfil1  23842  flimfil  23925  cldsubg  24067  tgpconncompeqg  24068  tgpconncomp  24069  tsmsxplem1  24109  utoptop  24190  unirnblps  24375  unirnbl  24376  setsmstopn  24434  tngtopn  24606  bndth  24925  bcthlem5  25296  ovolficcss  25438  ovollb  25448  voliunlem2  25520  voliunlem3  25521  uniioovol  25548  uniioombl  25558  opnmbllem  25570  ubthlem1  30957  hsupcl  31426  hsupss  31428  hsupunss  31430  hsupval2  31496  fnpreimac  32759  unicls  34080  pwsiga  34307  sigainb  34313  insiga  34314  pwldsys  34334  ddemeas  34413  omssubadd  34477  cvmsss2  35487  dfon2lem2  35995  ntruni  36540  clsint2  36542  neibastop1  36572  neibastop2lem  36573  neibastop3  36575  topmeet  36577  topjoin  36578  fnemeet1  36579  fnemeet2  36580  fnejoin1  36581  opnmbllem0  37901  heiborlem1  38056  elrfi  43045  pwpwuni  45411  0ome  46881