Theorem sspwuni 5043

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3890  𝒫 cpw 4542  ∪ cuni 4851

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 3432  df-ss 3907  df-pw 4544  df-uni 4852

This theorem is referenced by:  pwssb  5044  elpwpw  5045  elpwuni  5048  intss2  5051  rintn0  5052  dftr4  5199  uniixp  8862  fipwss  9335  dffi3  9337  uniwf  9734  numacn  9962  dfac12lem2  10058  fin23lem32  10257  isf34lem4  10290  isf34lem5  10291  fin1a2lem12  10324  itunitc1  10333  fpwwe2lem11  10555  tsksuc  10676  unirnioo  13393  restid  17387  mrcuni  17578  isacs3lem  18499  dmdprdd  19967  dprdfeq0  19990  dprdres  19996  dprdss  19997  dprdz  19998  subgdmdprd  20002  subgdprd  20003  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  ablfac1b  20038  lssintcl  20950  lbsextlem2  21149  lbsextlem3  21150  cssmre  21683  topgele  22905  topontopn  22915  unitg  22942  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  mretopd  23067  resttopon  23136  ordtuni  23165  conncompcld  23409  islocfin  23492  kgentopon  23513  txuni2  23540  ptuni2  23551  ptbasfi  23556  xkouni  23574  prdstopn  23603  txdis  23607  txcmplem2  23617  xkococnlem  23634  qtoptop2  23674  qtopuni  23677  tgqtop  23687  opnfbas  23817  neifil  23855  filunibas  23856  trfil1  23861  flimfil  23944  cldsubg  24086  tgpconncompeqg  24087  tgpconncomp  24088  tsmsxplem1  24128  utoptop  24209  unirnblps  24394  unirnbl  24395  setsmstopn  24453  tngtopn  24625  bndth  24935  bcthlem5  25305  ovolficcss  25446  ovollb  25456  voliunlem2  25528  voliunlem3  25529  uniioovol  25556  uniioombl  25566  opnmbllem  25578  ubthlem1  30956  hsupcl  31425  hsupss  31427  hsupunss  31429  hsupval2  31495  fnpreimac  32758  unicls  34063  pwsiga  34290  sigainb  34296  insiga  34297  pwldsys  34317  ddemeas  34396  omssubadd  34460  cvmsss2  35472  dfon2lem2  35980  ntruni  36525  clsint2  36527  neibastop1  36557  neibastop2lem  36558  neibastop3  36560  topmeet  36562  topjoin  36563  fnemeet1  36564  fnemeet2  36565  fnejoin1  36566  opnmbllem0  37991  heiborlem1  38146  elrfi  43140  pwpwuni  45506  0ome  46975