Theorem sspwuni 5060

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∀wral 3077   ⊆ wss 3899  𝒫 cpw 4557  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-pw 4559  df-uni 4868

This theorem is used by:  pwssb  5061  elpwpw  5062  elpwuni  5065  intss2  5068  rintn0  5069  dftr4  5218  uniixp  8933  fipwss  9405  dffi3  9407  uniwf  9809  numacn  10109  dfac12lem2  10204  fin23lem32  10403  isf34lem4  10436  isf34lem5  10437  fin1a2lem12  10470  itunitc1  10479  fpwwe2lem11  10707  tsksuc  10828  unirnioo  13561  restid  17584  mrcuni  17775  isacs3lem  18696  dmdprdd  20195  dprdfeq0  20218  dprdres  20224  dprdss  20225  dprdz  20226  subgdmdprd  20230  subgdprd  20231  dprd2dlem1  20237  dprd2da  20238  dmdprdsplit2lem  20241  ablfac1b  20266  lssintcl  21219  lbsextlem2  21417  lbsextlem3  21418  cssmre  21979  topgele  23228  topontopn  23238  unitg  23265  fctop  23302  cctop  23304  ppttop  23305  epttop  23307  mretopd  23390  resttopon  23459  ordtuni  23488  conncompcld  23732  islocfin  23816  kgentopon  23837  txuni2  23864  ptuni2  23875  ptbasfi  23880  xkouni  23898  prdstopn  23927  txdis  23931  txcmplem2  23941  xkococnlem  23958  qtoptop2  23998  qtopuni  24001  tgqtop  24011  opnfbas  24141  neifil  24179  filunibas  24180  trfil1  24185  flimfil  24268  cldsubg  24410  tgpconncompeqg  24411  tgpconncomp  24412  tsmsxplem1  24452  utoptop  24533  unirnblps  24718  unirnbl  24719  setsmstopn  24777  tngtopn  24949  bndth  25259  bcthlem5  25629  ovolficcss  25770  ovollb  25780  voliunlem2  25852  voliunlem3  25853  uniioovol  25880  uniioombl  25890  opnmbllem  25902  ubthlem1  31454  hsupcl  31923  hsupss  31925  hsupunss  31927  hsupval2  31993  fnpreimac  33246  unicls  34517  pwsiga  34744  sigainb  34751  insiga  34752  pwldsys  34772  ddemeas  34851  omssubadd  34915  cvmsss2  36008  dfon2lem2  36516  ntruni  37085  clsint2  37087  neibastop1  37117  neibastop2lem  37118  neibastop3  37120  topmeet  37122  topjoin  37123  fnemeet1  37124  fnemeet2  37125  fnejoin1  37126  opnmbllem0  38542  heiborlem1  38713  elrfi  43658  pwpwuni  46017  0ome  47483