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

Syntax hints:   ↔ wb 205   ∈ wcel 2104  ∀wral 3062   ⊆ wss 3892  𝒫 cpw 4539  ∪ cuni 4844

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-v 3439  df-in 3899  df-ss 3909  df-pw 4541  df-uni 4845

This theorem is referenced by:  pwssb  5037  elpwpw  5038  elpwuni  5041  intss2  5044  rintn0  5045  dftr4  5205  uniixp  8740  fipwss  9232  dffi3  9234  uniwf  9621  numacn  9851  dfac12lem2  9946  fin23lem32  10146  isf34lem4  10179  isf34lem5  10180  fin1a2lem12  10213  itunitc1  10222  fpwwe2lem11  10443  tsksuc  10564  unirnioo  13227  restid  17189  mrcuni  17375  isacs3lem  18305  dmdprdd  19647  dprdfeq0  19670  dprdres  19676  dprdss  19677  dprdz  19678  subgdmdprd  19682  subgdprd  19683  dprd2dlem1  19689  dprd2da  19690  dmdprdsplit2lem  19693  ablfac1b  19718  lssintcl  20271  lbsextlem2  20466  lbsextlem3  20467  cssmre  20943  topgele  22124  topontopn  22134  unitg  22162  fctop  22199  cctop  22201  ppttop  22202  epttop  22204  mretopd  22288  resttopon  22357  ordtuni  22386  conncompcld  22630  islocfin  22713  kgentopon  22734  txuni2  22761  ptuni2  22772  ptbasfi  22777  xkouni  22795  prdstopn  22824  txdis  22828  txcmplem2  22838  xkococnlem  22855  qtoptop2  22895  qtopuni  22898  tgqtop  22908  opnfbas  23038  neifil  23076  filunibas  23077  trfil1  23082  flimfil  23165  cldsubg  23307  tgpconncompeqg  23308  tgpconncomp  23309  tsmsxplem1  23349  utoptop  23431  unirnblps  23617  unirnbl  23618  setsmstopn  23678  tngtopn  23859  bndth  24166  bcthlem5  24537  ovolficcss  24678  ovollb  24688  voliunlem2  24760  voliunlem3  24761  uniioovol  24788  uniioombl  24798  opnmbllem  24810  ubthlem1  29277  hsupcl  29746  hsupss  29748  hsupunss  29750  hsupval2  29816  fnpreimac  31053  unicls  31898  pwsiga  32143  sigainb  32149  insiga  32150  pwldsys  32170  ddemeas  32249  omssubadd  32312  cvmsss2  33281  dfon2lem2  33805  ntruni  34561  clsint2  34563  neibastop1  34593  neibastop2lem  34594  neibastop3  34596  topmeet  34598  topjoin  34599  fnemeet1  34600  fnemeet2  34601  fnejoin1  34602  opnmbllem0  35857  heiborlem1  36013  elrfi  40553  pwpwuni  42643  0ome  44117