Theorem sspwuni 5059

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 4561	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3108	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3897	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4900	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895  𝒫 cpw 4556  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867

This theorem is used by:  pwssb  5060  elpwpw  5061  elpwuni  5064  intss2  5067  rintn0  5068  dftr4  5217  uniixp  8949  fipwss  9421  dffi3  9423  uniwf  9828  numacn  10128  dfac12lem2  10223  fin23lem32  10422  isf34lem4  10455  isf34lem5  10456  fin1a2lem12  10489  itunitc1  10498  fpwwe2lem11  10726  tsksuc  10847  unirnioo  13580  restid  17604  mrcuni  17795  isacs3lem  18716  dmdprdd  20215  dprdfeq0  20238  dprdres  20244  dprdss  20245  dprdz  20246  subgdmdprd  20250  subgdprd  20251  dprd2dlem1  20257  dprd2da  20258  dmdprdsplit2lem  20261  ablfac1b  20286  lssintcl  21239  lbsextlem2  21437  lbsextlem3  21438  cssmre  21999  topgele  23248  topontopn  23258  unitg  23285  fctop  23322  cctop  23324  ppttop  23325  epttop  23327  mretopd  23410  resttopon  23479  ordtuni  23508  conncompcld  23752  islocfin  23836  kgentopon  23857  txuni2  23884  ptuni2  23895  ptbasfi  23900  xkouni  23918  prdstopn  23947  txdis  23951  txcmplem2  23961  xkococnlem  23978  qtoptop2  24018  qtopuni  24021  tgqtop  24031  opnfbas  24161  neifil  24199  filunibas  24200  trfil1  24205  flimfil  24288  cldsubg  24430  tgpconncompeqg  24431  tgpconncomp  24432  tsmsxplem1  24472  utoptop  24553  unirnblps  24738  unirnbl  24739  setsmstopn  24797  tngtopn  24969  bndth  25279  bcthlem5  25649  ovolficcss  25790  ovollb  25800  voliunlem2  25872  voliunlem3  25873  uniioovol  25900  uniioombl  25910  opnmbllem  25922  ubthlem1  31472  hsupcl  31941  hsupss  31943  hsupunss  31945  hsupval2  32011  fnpreimac  33306  unicls  34577  pwsiga  34804  sigainb  34811  insiga  34812  pwldsys  34832  ddemeas  34911  omssubadd  34974  cvmsss2  36081  dfon2lem2  36588  ntruni  37157  clsint2  37159  neibastop1  37189  neibastop2lem  37190  neibastop3  37192  topmeet  37194  topjoin  37195  fnemeet1  37196  fnemeet2  37197  fnejoin1  37198  opnmbllem0  38617  heiborlem1  38788  elrfi  43747  pwpwuni  46116  0ome  47581