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 4568	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
2	1	ralbii 3075	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
3		dfss3 3935	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝒫 𝐵)
4		unissb 4903	. 2 ⊢ (∪ 𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵)
5	2, 3, 4	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3044   ⊆ wss 3914  𝒫 cpw 4563  ∪ cuni 4871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-ss 3931  df-pw 4565  df-uni 4872

This theorem is referenced by:  pwssb  5065  elpwpw  5066  elpwuni  5069  intss2  5072  rintn0  5073  dftr4  5221  uniixp  8894  fipwss  9380  dffi3  9382  uniwf  9772  numacn  10002  dfac12lem2  10098  fin23lem32  10297  isf34lem4  10330  isf34lem5  10331  fin1a2lem12  10364  itunitc1  10373  fpwwe2lem11  10594  tsksuc  10715  unirnioo  13410  restid  17396  mrcuni  17582  isacs3lem  18501  dmdprdd  19931  dprdfeq0  19954  dprdres  19960  dprdss  19961  dprdz  19962  subgdmdprd  19966  subgdprd  19967  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  ablfac1b  20002  lssintcl  20870  lbsextlem2  21069  lbsextlem3  21070  cssmre  21602  topgele  22817  topontopn  22827  unitg  22854  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  mretopd  22979  resttopon  23048  ordtuni  23077  conncompcld  23321  islocfin  23404  kgentopon  23425  txuni2  23452  ptuni2  23463  ptbasfi  23468  xkouni  23486  prdstopn  23515  txdis  23519  txcmplem2  23529  xkococnlem  23546  qtoptop2  23586  qtopuni  23589  tgqtop  23599  opnfbas  23729  neifil  23767  filunibas  23768  trfil1  23773  flimfil  23856  cldsubg  23998  tgpconncompeqg  23999  tgpconncomp  24000  tsmsxplem1  24040  utoptop  24122  unirnblps  24307  unirnbl  24308  setsmstopn  24366  tngtopn  24538  bndth  24857  bcthlem5  25228  ovolficcss  25370  ovollb  25380  voliunlem2  25452  voliunlem3  25453  uniioovol  25480  uniioombl  25490  opnmbllem  25502  ubthlem1  30799  hsupcl  31268  hsupss  31270  hsupunss  31272  hsupval2  31338  fnpreimac  32595  unicls  33893  pwsiga  34120  sigainb  34126  insiga  34127  pwldsys  34147  ddemeas  34226  omssubadd  34291  cvmsss2  35261  dfon2lem2  35772  ntruni  36315  clsint2  36317  neibastop1  36347  neibastop2lem  36348  neibastop3  36350  topmeet  36352  topjoin  36353  fnemeet1  36354  fnemeet2  36355  fnejoin1  36356  opnmbllem0  37650  heiborlem1  37805  elrfi  42682  pwpwuni  45051  0ome  46527