Theorem sspwuni 5100

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∀wral 3061   ⊆ wss 3951  𝒫 cpw 4600  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-v 3482  df-ss 3968  df-pw 4602  df-uni 4908

This theorem is referenced by:  pwssb  5101  elpwpw  5102  elpwuni  5105  intss2  5108  rintn0  5109  dftr4  5266  uniixp  8961  fipwss  9469  dffi3  9471  uniwf  9859  numacn  10089  dfac12lem2  10185  fin23lem32  10384  isf34lem4  10417  isf34lem5  10418  fin1a2lem12  10451  itunitc1  10460  fpwwe2lem11  10681  tsksuc  10802  unirnioo  13489  restid  17478  mrcuni  17664  isacs3lem  18587  dmdprdd  20019  dprdfeq0  20042  dprdres  20048  dprdss  20049  dprdz  20050  subgdmdprd  20054  subgdprd  20055  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  ablfac1b  20090  lssintcl  20962  lbsextlem2  21161  lbsextlem3  21162  cssmre  21711  topgele  22936  topontopn  22946  unitg  22974  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  mretopd  23100  resttopon  23169  ordtuni  23198  conncompcld  23442  islocfin  23525  kgentopon  23546  txuni2  23573  ptuni2  23584  ptbasfi  23589  xkouni  23607  prdstopn  23636  txdis  23640  txcmplem2  23650  xkococnlem  23667  qtoptop2  23707  qtopuni  23710  tgqtop  23720  opnfbas  23850  neifil  23888  filunibas  23889  trfil1  23894  flimfil  23977  cldsubg  24119  tgpconncompeqg  24120  tgpconncomp  24121  tsmsxplem1  24161  utoptop  24243  unirnblps  24429  unirnbl  24430  setsmstopn  24490  tngtopn  24671  bndth  24990  bcthlem5  25362  ovolficcss  25504  ovollb  25514  voliunlem2  25586  voliunlem3  25587  uniioovol  25614  uniioombl  25624  opnmbllem  25636  ubthlem1  30889  hsupcl  31358  hsupss  31360  hsupunss  31362  hsupval2  31428  fnpreimac  32681  unicls  33902  pwsiga  34131  sigainb  34137  insiga  34138  pwldsys  34158  ddemeas  34237  omssubadd  34302  cvmsss2  35279  dfon2lem2  35785  ntruni  36328  clsint2  36330  neibastop1  36360  neibastop2lem  36361  neibastop3  36363  topmeet  36365  topjoin  36366  fnemeet1  36367  fnemeet2  36368  fnejoin1  36369  opnmbllem0  37663  heiborlem1  37818  elrfi  42705  pwpwuni  45062  0ome  46544