Theorem sspwuni 5063

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  ∀wral 3080   ⊆ wss 3900  𝒫 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-ss 3901  df-pw 4562  df-uni 4871

This theorem is used by:  pwssb  5064  elpwpw  5065  elpwuni  5068  intss2  5071  rintn0  5072  dftr4  5222  uniixp  8980  fipwss  9451  dffi3  9453  uniwf  9858  numacn  10158  dfac12lem2  10253  fin23lem32  10452  isf34lem4  10485  isf34lem5  10486  fin1a2lem12  10519  itunitc1  10528  fpwwe2lem11  10756  tsksuc  10877  unirnioo  13610  restid  17636  mrcuni  17827  isacs3lem  18748  dmdprdd  20248  dprdfeq0  20271  dprdres  20277  dprdss  20278  dprdz  20279  subgdmdprd  20283  subgdprd  20284  dprd2dlem1  20290  dprd2da  20291  dmdprdsplit2lem  20294  ablfac1b  20319  lssintcl  21272  lbsextlem2  21470  lbsextlem3  21471  cssmre  22032  topgele  23281  topontopn  23291  unitg  23318  fctop  23355  cctop  23357  ppttop  23358  epttop  23360  mretopd  23443  resttopon  23512  ordtuni  23541  conncompcld  23785  islocfin  23869  kgentopon  23890  txuni2  23917  ptuni2  23928  ptbasfi  23933  xkouni  23951  prdstopn  23980  txdis  23984  txcmplem2  23994  xkococnlem  24011  qtoptop2  24051  qtopuni  24054  tgqtop  24064  opnfbas  24194  neifil  24232  filunibas  24233  trfil1  24238  flimfil  24321  cldsubg  24463  tgpconncompeqg  24464  tgpconncomp  24465  tsmsxplem1  24505  utoptop  24586  unirnblps  24771  unirnbl  24772  setsmstopn  24830  tngtopn  25002  bndth  25312  bcthlem5  25682  ovolficcss  25823  ovollb  25833  voliunlem2  25905  voliunlem3  25906  uniioovol  25933  uniioombl  25943  opnmbllem  25955  ubthlem1  31505  hsupcl  31974  hsupss  31976  hsupunss  31978  hsupval2  32044  fnpreimac  33339  reff  34554  unicls  34618  pwsiga  34845  sigainb  34852  insiga  34853  pwldsys  34873  ddemeas  34952  omssubadd  35015  cvmsss2  36219  dfon2lem2  36737  ntruni  37306  clsint2  37308  neibastop1  37338  neibastop2lem  37339  neibastop3  37341  topmeet  37343  topjoin  37344  fnemeet1  37345  fnemeet2  37346  fnejoin1  37347  opnmbllem0  38779  heiborlem1  38948  elrfi  43909  pwpwuni  46290  0ome  47754