Theorem sspwuni 5021

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 4543	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3165	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3955	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4869	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 208   ∈ wcel 2110  ∀wral 3138   ⊆ wss 3935  𝒫 cpw 4538  ∪ cuni 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-v 3496  df-in 3942  df-ss 3951  df-pw 4540  df-uni 4838

This theorem is referenced by:  pwssb  5022  elpwpw  5023  elpwuni  5026  rintn0  5029  dftr4  5176  uniixp  8484  fipwss  8892  dffi3  8894  uniwf  9247  numacn  9474  dfac12lem2  9569  fin23lem32  9765  isf34lem4  9798  isf34lem5  9799  fin1a2lem12  9832  itunitc1  9841  fpwwe2lem12  10062  tsksuc  10183  unirnioo  12836  restid  16706  mrcuni  16891  isacs3lem  17775  dmdprdd  19120  dprdfeq0  19143  dprdres  19149  dprdss  19150  dprdz  19151  subgdmdprd  19155  subgdprd  19156  dprd2dlem1  19162  dprd2da  19163  dmdprdsplit2lem  19166  ablfac1b  19191  lssintcl  19735  lbsextlem2  19930  lbsextlem3  19931  cssmre  20836  topgele  21537  topontopn  21547  unitg  21574  fctop  21611  cctop  21613  ppttop  21614  epttop  21616  mretopd  21699  resttopon  21768  ordtuni  21797  conncompcld  22041  islocfin  22124  kgentopon  22145  txuni2  22172  ptuni2  22183  ptbasfi  22188  xkouni  22206  prdstopn  22235  txdis  22239  txcmplem2  22249  xkococnlem  22266  qtoptop2  22306  qtopuni  22309  tgqtop  22319  opnfbas  22449  neifil  22487  filunibas  22488  trfil1  22493  flimfil  22576  cldsubg  22718  tgpconncompeqg  22719  tgpconncomp  22720  tsmsxplem1  22760  utoptop  22842  unirnblps  23028  unirnbl  23029  setsmstopn  23087  tngtopn  23258  bndth  23561  bcthlem5  23930  ovolficcss  24069  ovollb  24079  voliunlem2  24151  voliunlem3  24152  uniioovol  24179  uniioombl  24189  opnmbllem  24201  ubthlem1  28646  hsupcl  29115  hsupss  29117  hsupunss  29119  hsupval2  29185  fnpreimac  30415  unicls  31146  pwsiga  31389  sigainb  31395  insiga  31396  pwldsys  31416  ddemeas  31495  omssubadd  31558  cvmsss2  32521  dfon2lem2  33029  ntruni  33675  clsint2  33677  neibastop1  33707  neibastop2lem  33708  neibastop3  33710  topmeet  33712  topjoin  33713  fnemeet1  33714  fnemeet2  33715  fnejoin1  33716  bj-intss  34390  opnmbllem0  34927  heiborlem1  35088  elrfi  39289  pwpwuni  41317  0ome  42810