Theorem sspwuni 5042

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3051   ⊆ wss 3889  𝒫 cpw 4541  ∪ cuni 4850

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-ss 3906  df-pw 4543  df-uni 4851

This theorem is referenced by:  pwssb  5043  elpwpw  5044  elpwuni  5047  intss2  5050  rintn0  5051  dftr4  5198  uniixp  8869  fipwss  9342  dffi3  9344  uniwf  9743  numacn  9971  dfac12lem2  10067  fin23lem32  10266  isf34lem4  10299  isf34lem5  10300  fin1a2lem12  10333  itunitc1  10342  fpwwe2lem11  10564  tsksuc  10685  unirnioo  13402  restid  17396  mrcuni  17587  isacs3lem  18508  dmdprdd  19976  dprdfeq0  19999  dprdres  20005  dprdss  20006  dprdz  20007  subgdmdprd  20011  subgdprd  20012  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  ablfac1b  20047  lssintcl  20959  lbsextlem2  21157  lbsextlem3  21158  cssmre  21673  topgele  22895  topontopn  22905  unitg  22932  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  mretopd  23057  resttopon  23126  ordtuni  23155  conncompcld  23399  islocfin  23482  kgentopon  23503  txuni2  23530  ptuni2  23541  ptbasfi  23546  xkouni  23564  prdstopn  23593  txdis  23597  txcmplem2  23607  xkococnlem  23624  qtoptop2  23664  qtopuni  23667  tgqtop  23677  opnfbas  23807  neifil  23845  filunibas  23846  trfil1  23851  flimfil  23934  cldsubg  24076  tgpconncompeqg  24077  tgpconncomp  24078  tsmsxplem1  24118  utoptop  24199  unirnblps  24384  unirnbl  24385  setsmstopn  24443  tngtopn  24615  bndth  24925  bcthlem5  25295  ovolficcss  25436  ovollb  25446  voliunlem2  25518  voliunlem3  25519  uniioovol  25546  uniioombl  25556  opnmbllem  25568  ubthlem1  30941  hsupcl  31410  hsupss  31412  hsupunss  31414  hsupval2  31480  fnpreimac  32743  unicls  34047  pwsiga  34274  sigainb  34280  insiga  34281  pwldsys  34301  ddemeas  34380  omssubadd  34444  cvmsss2  35456  dfon2lem2  35964  ntruni  36509  clsint2  36511  neibastop1  36541  neibastop2lem  36542  neibastop3  36544  topmeet  36546  topjoin  36547  fnemeet1  36548  fnemeet2  36549  fnejoin1  36550  opnmbllem0  37977  heiborlem1  38132  elrfi  43126  pwpwuni  45488  0ome  46957