Theorem sspwuni 5056

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3052   ⊆ wss 3902  𝒫 cpw 4555  ∪ cuni 4864

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 3443  df-ss 3919  df-pw 4557  df-uni 4865

This theorem is referenced by:  pwssb  5057  elpwpw  5058  elpwuni  5061  intss2  5064  rintn0  5065  dftr4  5212  uniixp  8863  fipwss  9336  dffi3  9338  uniwf  9735  numacn  9963  dfac12lem2  10059  fin23lem32  10258  isf34lem4  10291  isf34lem5  10292  fin1a2lem12  10325  itunitc1  10334  fpwwe2lem11  10556  tsksuc  10677  unirnioo  13369  restid  17357  mrcuni  17548  isacs3lem  18469  dmdprdd  19934  dprdfeq0  19957  dprdres  19963  dprdss  19964  dprdz  19965  subgdmdprd  19969  subgdprd  19970  dprd2dlem1  19976  dprd2da  19977  dmdprdsplit2lem  19980  ablfac1b  20005  lssintcl  20919  lbsextlem2  21118  lbsextlem3  21119  cssmre  21652  topgele  22878  topontopn  22888  unitg  22915  fctop  22952  cctop  22954  ppttop  22955  epttop  22957  mretopd  23040  resttopon  23109  ordtuni  23138  conncompcld  23382  islocfin  23465  kgentopon  23486  txuni2  23513  ptuni2  23524  ptbasfi  23529  xkouni  23547  prdstopn  23576  txdis  23580  txcmplem2  23590  xkococnlem  23607  qtoptop2  23647  qtopuni  23650  tgqtop  23660  opnfbas  23790  neifil  23828  filunibas  23829  trfil1  23834  flimfil  23917  cldsubg  24059  tgpconncompeqg  24060  tgpconncomp  24061  tsmsxplem1  24101  utoptop  24182  unirnblps  24367  unirnbl  24368  setsmstopn  24426  tngtopn  24598  bndth  24917  bcthlem5  25288  ovolficcss  25430  ovollb  25440  voliunlem2  25512  voliunlem3  25513  uniioovol  25540  uniioombl  25550  opnmbllem  25562  ubthlem1  30928  hsupcl  31397  hsupss  31399  hsupunss  31401  hsupval2  31467  fnpreimac  32730  unicls  34041  pwsiga  34268  sigainb  34274  insiga  34275  pwldsys  34295  ddemeas  34374  omssubadd  34438  cvmsss2  35449  dfon2lem2  35957  ntruni  36502  clsint2  36504  neibastop1  36534  neibastop2lem  36535  neibastop3  36537  topmeet  36539  topjoin  36540  fnemeet1  36541  fnemeet2  36542  fnejoin1  36543  opnmbllem0  37828  heiborlem1  37983  elrfi  42972  pwpwuni  45338  0ome  46809