Theorem sspwuni 5064

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∀wral 3078   ⊆ wss 3902  𝒫 cpw 4560  ∪ cuni 4870

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-v 3455  df-ss 3919  df-pw 4562  df-uni 4871

This theorem is used by:  pwssb  5065  elpwpw  5066  elpwuni  5069  intss2  5072  rintn0  5073  dftr4  5222  uniixp  8932  fipwss  9403  dffi3  9405  uniwf  9805  numacn  10056  dfac12lem2  10151  fin23lem32  10350  isf34lem4  10383  isf34lem5  10384  fin1a2lem12  10417  itunitc1  10426  fpwwe2lem11  10654  tsksuc  10775  unirnioo  13506  restid  17524  mrcuni  17715  isacs3lem  18636  dmdprdd  20134  dprdfeq0  20157  dprdres  20163  dprdss  20164  dprdz  20165  subgdmdprd  20169  subgdprd  20170  dprd2dlem1  20176  dprd2da  20177  dmdprdsplit2lem  20180  ablfac1b  20205  lssintcl  21154  lbsextlem2  21352  lbsextlem3  21353  cssmre  21912  topgele  23161  topontopn  23171  unitg  23198  fctop  23235  cctop  23237  ppttop  23238  epttop  23240  mretopd  23323  resttopon  23392  ordtuni  23421  conncompcld  23665  islocfin  23749  kgentopon  23770  txuni2  23797  ptuni2  23808  ptbasfi  23813  xkouni  23831  prdstopn  23860  txdis  23864  txcmplem2  23874  xkococnlem  23891  qtoptop2  23931  qtopuni  23934  tgqtop  23944  opnfbas  24074  neifil  24112  filunibas  24113  trfil1  24118  flimfil  24201  cldsubg  24343  tgpconncompeqg  24344  tgpconncomp  24345  tsmsxplem1  24385  utoptop  24466  unirnblps  24651  unirnbl  24652  setsmstopn  24710  tngtopn  24882  bndth  25192  bcthlem5  25562  ovolficcss  25703  ovollb  25713  voliunlem2  25785  voliunlem3  25786  uniioovol  25813  uniioombl  25823  opnmbllem  25835  ubthlem1  31359  hsupcl  31828  hsupss  31830  hsupunss  31832  hsupval2  31898  fnpreimac  33151  unicls  34421  pwsiga  34648  sigainb  34655  insiga  34656  pwldsys  34676  ddemeas  34755  omssubadd  34819  cvmsss2  35861  dfon2lem2  36369  ntruni  36954  clsint2  36956  neibastop1  36986  neibastop2lem  36987  neibastop3  36989  topmeet  36991  topjoin  36992  fnemeet1  36993  fnemeet2  36994  fnejoin1  36995  opnmbllem0  38413  heiborlem1  38569  elrfi  43547  pwpwuni  45899  0ome  47365