Theorem sspwuni 5050

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∀wral 3048   ⊆ wss 3898  𝒫 cpw 4549  ∪ cuni 4858

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-v 3439  df-ss 3915  df-pw 4551  df-uni 4859

This theorem is referenced by:  pwssb  5051  elpwpw  5052  elpwuni  5055  intss2  5058  rintn0  5059  dftr4  5206  uniixp  8851  fipwss  9320  dffi3  9322  uniwf  9719  numacn  9947  dfac12lem2  10043  fin23lem32  10242  isf34lem4  10275  isf34lem5  10276  fin1a2lem12  10309  itunitc1  10318  fpwwe2lem11  10539  tsksuc  10660  unirnioo  13351  restid  17339  mrcuni  17529  isacs3lem  18450  dmdprdd  19915  dprdfeq0  19938  dprdres  19944  dprdss  19945  dprdz  19946  subgdmdprd  19950  subgdprd  19951  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  ablfac1b  19986  lssintcl  20899  lbsextlem2  21098  lbsextlem3  21099  cssmre  21632  topgele  22846  topontopn  22856  unitg  22883  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  mretopd  23008  resttopon  23077  ordtuni  23106  conncompcld  23350  islocfin  23433  kgentopon  23454  txuni2  23481  ptuni2  23492  ptbasfi  23497  xkouni  23515  prdstopn  23544  txdis  23548  txcmplem2  23558  xkococnlem  23575  qtoptop2  23615  qtopuni  23618  tgqtop  23628  opnfbas  23758  neifil  23796  filunibas  23797  trfil1  23802  flimfil  23885  cldsubg  24027  tgpconncompeqg  24028  tgpconncomp  24029  tsmsxplem1  24069  utoptop  24150  unirnblps  24335  unirnbl  24336  setsmstopn  24394  tngtopn  24566  bndth  24885  bcthlem5  25256  ovolficcss  25398  ovollb  25408  voliunlem2  25480  voliunlem3  25481  uniioovol  25508  uniioombl  25518  opnmbllem  25530  ubthlem1  30852  hsupcl  31321  hsupss  31323  hsupunss  31325  hsupval2  31391  fnpreimac  32655  unicls  33937  pwsiga  34164  sigainb  34170  insiga  34171  pwldsys  34191  ddemeas  34270  omssubadd  34334  cvmsss2  35339  dfon2lem2  35847  ntruni  36392  clsint2  36394  neibastop1  36424  neibastop2lem  36425  neibastop3  36427  topmeet  36429  topjoin  36430  fnemeet1  36431  fnemeet2  36432  fnejoin1  36433  opnmbllem0  37716  heiborlem1  37871  elrfi  42811  pwpwuni  45178  0ome  46651