Theorem sspwuni 5062

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

Syntax hints:   ↔ wb 209   ∈ wcel 2145  ∀wral 3079   ⊆ wss 3907  𝒫 cpw 4558  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-ss 3924  df-pw 4560  df-uni 4869

This theorem is referenced by:  pwssb  5063  elpwpw  5064  elpwuni  5067  intss2  5070  rintn0  5071  dftr4  5218  uniixp  8907  fipwss  9377  dffi3  9379  uniwf  9779  numacn  10021  dfac12lem2  10116  fin23lem32  10316  isf34lem4  10349  isf34lem5  10350  fin1a2lem12  10383  itunitc1  10392  fpwwe2lem11  10614  tsksuc  10735  unirnioo  13467  restid  17476  mrcuni  17667  isacs3lem  18588  dmdprdd  20062  dprdfeq0  20085  dprdres  20091  dprdss  20092  dprdz  20093  subgdmdprd  20097  subgdprd  20098  dprd2dlem1  20104  dprd2da  20105  dmdprdsplit2lem  20108  ablfac1b  20133  lssintcl  21054  lbsextlem2  21252  lbsextlem3  21253  cssmre  21803  topgele  23048  topontopn  23058  unitg  23085  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  mretopd  23210  resttopon  23279  ordtuni  23308  conncompcld  23552  islocfin  23635  kgentopon  23656  txuni2  23683  ptuni2  23694  ptbasfi  23699  xkouni  23717  prdstopn  23746  txdis  23750  txcmplem2  23760  xkococnlem  23777  qtoptop2  23817  qtopuni  23820  tgqtop  23830  opnfbas  23960  neifil  23998  filunibas  23999  trfil1  24004  flimfil  24087  cldsubg  24229  tgpconncompeqg  24230  tgpconncomp  24231  tsmsxplem1  24271  utoptop  24352  unirnblps  24537  unirnbl  24538  setsmstopn  24596  tngtopn  24768  bndth  25078  bcthlem5  25448  ovolficcss  25589  ovollb  25599  voliunlem2  25671  voliunlem3  25672  uniioovol  25699  uniioombl  25709  opnmbllem  25721  ubthlem1  31131  hsupcl  31600  hsupss  31602  hsupunss  31604  hsupval2  31670  fnpreimac  32927  unicls  34210  pwsiga  34437  sigainb  34443  insiga  34444  pwldsys  34464  ddemeas  34543  omssubadd  34607  cvmsss2  35637  dfon2lem2  36145  ntruni  36700  clsint2  36702  neibastop1  36732  neibastop2lem  36733  neibastop3  36735  topmeet  36737  topjoin  36738  fnemeet1  36739  fnemeet2  36740  fnejoin1  36741  opnmbllem0  38167  heiborlem1  38322  elrfi  43287  pwpwuni  45635  0ome  47101