Theorem sspwuni 5036

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  ∀wral 3054   ⊆ wss 3890  𝒫 cpw 4536  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-v 3434  df-ss 3907  df-pw 4538  df-uni 4846

This theorem is referenced by:  pwssb  5037  elpwpw  5038  elpwuni  5041  intss2  5044  rintn0  5045  dftr4  5192  uniixp  8866  fipwss  9339  dffi3  9341  uniwf  9741  numacn  9969  dfac12lem2  10065  fin23lem32  10264  isf34lem4  10297  isf34lem5  10298  fin1a2lem12  10331  itunitc1  10340  fpwwe2lem11  10562  tsksuc  10683  unirnioo  13400  restid  17394  mrcuni  17585  isacs3lem  18506  dmdprdd  19974  dprdfeq0  19997  dprdres  20003  dprdss  20004  dprdz  20005  subgdmdprd  20009  subgdprd  20010  dprd2dlem1  20016  dprd2da  20017  dmdprdsplit2lem  20020  ablfac1b  20045  lssintcl  20961  lbsextlem2  21159  lbsextlem3  21160  cssmre  21675  topgele  22920  topontopn  22930  unitg  22957  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  mretopd  23082  resttopon  23151  ordtuni  23180  conncompcld  23424  islocfin  23507  kgentopon  23528  txuni2  23555  ptuni2  23566  ptbasfi  23571  xkouni  23589  prdstopn  23618  txdis  23622  txcmplem2  23632  xkococnlem  23649  qtoptop2  23689  qtopuni  23692  tgqtop  23702  opnfbas  23832  neifil  23870  filunibas  23871  trfil1  23876  flimfil  23959  cldsubg  24101  tgpconncompeqg  24102  tgpconncomp  24103  tsmsxplem1  24143  utoptop  24224  unirnblps  24409  unirnbl  24410  setsmstopn  24468  tngtopn  24640  bndth  24950  bcthlem5  25320  ovolficcss  25461  ovollb  25471  voliunlem2  25543  voliunlem3  25544  uniioovol  25571  uniioombl  25581  opnmbllem  25593  ubthlem1  30966  hsupcl  31435  hsupss  31437  hsupunss  31439  hsupval2  31505  fnpreimac  32769  unicls  34094  pwsiga  34321  sigainb  34327  insiga  34328  pwldsys  34348  ddemeas  34427  omssubadd  34491  cvmsss2  35509  dfon2lem2  36017  ntruni  36562  clsint2  36564  neibastop1  36594  neibastop2lem  36595  neibastop3  36597  topmeet  36599  topjoin  36600  fnemeet1  36601  fnemeet2  36602  fnejoin1  36603  opnmbllem0  38030  heiborlem1  38185  elrfi  43150  pwpwuni  45512  0ome  46979