Theorem unss 3677

Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)

Assertion

Ref	Expression
unss

Proof of Theorem unss

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3492	. 2
2		19.26 1680	. . 3
3		elun 3644	. . . . . 6
4	3	imbi1i 325	. . . . 5
5		jaob 783	. . . . 5
6	4, 5	bitri 249	. . . 4
7	6	albii 1640	. . 3
8		dfss2 3492	. . . 4
9		dfss2 3492	. . . 4
10	8, 9	anbi12i 697	. . 3
11	2, 7, 10	3bitr4i 277	. 2
12	1, 11	bitr2i 250	1

Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  A.wal 1393  e.wcel 1818  u.cun 3473  C_wss 3475

This theorem is referenced by:  unssi  3678  unssd  3679  unssad  3680  unssbd  3681  nsspssun  3730  uneqin  3748  uneqdifeq  3916  prss  4184  prssg  4185  ssunsn2  4189  tpss  4195  pwundif  4792  eqrelrel  5109  xpsspw  5121  xpsspwOLD  5122  relun  5124  relcoi2  5540  fnsuppresOLD  6131  fnsuppres  6946  dfer2  7331  isinf  7753  fiin  7902  trcl  8180  supxrun  11536  isumltss  13660  rpnnen2  13959  lubun  15753  isipodrs  15791  fpwipodrs  15794  ipodrsima  15795  aspval2  17996  unocv  18711  uncld  19542  restntr  19683  cmpcld  19902  uncmp  19903  ufprim  20410  tsmsfbas  20626  ovolctb2  21903  ovolun  21910  unmbl  21948  plyun0  22594  sshjcl  26273  sshjval2  26329  shlub  26332  ssjo  26365  spanuni  26462  dfon2lem3  29217  dfon2lem7  29221  wfrlem15  29357  mblfinlem3  30053  ismblfin  30055  clsun  30146  lsmfgcl  31020  paddssat  35538  pclunN  35622  paddunN  35651  poldmj1N  35652  pclfinclN  35674  ssuncl  37755  sssymdifcl  37757  unhe1  37808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489