Theorem sspwuni 5071

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  ∀wral 3082   ⊆ wss 3908  𝒫 cpw 4567  ∪ cuni 4877

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-v 3460  df-ss 3925  df-pw 4569  df-uni 4878

This theorem is used by:  pwssb  5072  elpwpw  5073  elpwuni  5076  intss2  5079  rintn0  5080  dftr4  5229  uniixp  8928  fipwss  9399  dffi3  9401  uniwf  9801  numacn  10052  dfac12lem2  10147  fin23lem32  10346  isf34lem4  10379  isf34lem5  10380  fin1a2lem12  10413  itunitc1  10422  fpwwe2lem11  10644  tsksuc  10765  unirnioo  13494  restid  17511  mrcuni  17702  isacs3lem  18623  dmdprdd  20102  dprdfeq0  20125  dprdres  20131  dprdss  20132  dprdz  20133  subgdmdprd  20137  subgdprd  20138  dprd2dlem1  20144  dprd2da  20145  dmdprdsplit2lem  20148  ablfac1b  20173  lssintcl  21122  lbsextlem2  21320  lbsextlem3  21321  cssmre  21880  topgele  23124  topontopn  23134  unitg  23161  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  mretopd  23286  resttopon  23355  ordtuni  23384  conncompcld  23628  islocfin  23711  kgentopon  23732  txuni2  23759  ptuni2  23770  ptbasfi  23775  xkouni  23793  prdstopn  23822  txdis  23826  txcmplem2  23836  xkococnlem  23853  qtoptop2  23893  qtopuni  23896  tgqtop  23906  opnfbas  24036  neifil  24074  filunibas  24075  trfil1  24080  flimfil  24163  cldsubg  24305  tgpconncompeqg  24306  tgpconncomp  24307  tsmsxplem1  24347  utoptop  24428  unirnblps  24613  unirnbl  24614  setsmstopn  24672  tngtopn  24844  bndth  25154  bcthlem5  25524  ovolficcss  25665  ovollb  25675  voliunlem2  25747  voliunlem3  25748  uniioovol  25775  uniioombl  25785  opnmbllem  25797  ubthlem1  31259  hsupcl  31728  hsupss  31730  hsupunss  31732  hsupval2  31798  fnpreimac  33052  unicls  34324  pwsiga  34551  sigainb  34558  insiga  34559  pwldsys  34579  ddemeas  34658  omssubadd  34722  cvmsss2  35787  dfon2lem2  36295  ntruni  36879  clsint2  36881  neibastop1  36911  neibastop2lem  36912  neibastop3  36914  topmeet  36916  topjoin  36917  fnemeet1  36918  fnemeet2  36919  fnejoin1  36920  opnmbllem0  38348  heiborlem1  38503  elrfi  43466  pwpwuni  45818  0ome  47284