Theorem unss 3608

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	|- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )

Proof of Theorem unss

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss2 3421	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1732	. . 3 |- ( A. x ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) <-> ( A. x ( x e. A -> x e. C ) /\ A. x ( x e. B -> x e. C ) ) )
3		elun 3574	. . . . . 6 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	imbi1i 327	. . . . 5 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A \/ x e. B ) -> x e. C ) )
5		jaob 792	. . . . 5 |- ( ( ( x e. A \/ x e. B ) -> x e. C ) <-> ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
6	4, 5	bitri 253	. . . 4 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
7	6	albii 1691	. . 3 |- ( A. x ( x e. ( A u. B ) -> x e. C ) <-> A. x ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
8		dfss2 3421	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3421	. . . 4 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
10	8, 9	anbi12i 703	. . 3 |- ( ( A C_ C /\ B C_ C ) <-> ( A. x ( x e. A -> x e. C ) /\ A. x ( x e. B -> x e. C ) ) )
11	2, 7, 10	3bitr4i 281	. 2 |- ( A. x ( x e. ( A u. B ) -> x e. C ) <-> ( A C_ C /\ B C_ C ) )
12	1, 11	bitr2i 254	1 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   A.wal 1442   e. wcel 1887   u. cun 3402   C_ wss 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409  df-in 3411  df-ss 3418

This theorem is referenced by:  unssi  3609  unssd  3610  unssad  3611  unssbd  3612  nsspssun  3676  uneqin  3694  uneqdifeq  3856  prss  4126  prssg  4127  ssunsn2  4131  tpss  4137  pwundif  4741  eqrelrel  4936  xpsspw  4948  relun  4950  relcoi2  5363  fnsuppres  6942  wfrlem15  7050  dfer2  7364  isinf  7785  fiin  7936  trcl  8212  supxrun  11601  trclun  13078  isumltss  13906  rpnnen2  14278  lcmfunsnlem  14614  lcmfun  14618  coprmprod  14678  coprmproddvdslem  14679  lubun  16369  isipodrs  16407  fpwipodrs  16410  ipodrsima  16411  aspval2  18571  unocv  19243  uncld  20056  restntr  20198  cmpcld  20417  uncmp  20418  ufprim  20924  tsmsfbas  21142  ovolctb2  22445  ovolun  22452  unmbl  22491  plyun0  23151  sshjcl  27008  sshjval2  27064  shlub  27067  ssjo  27100  spanuni  27197  dfon2lem3  30431  dfon2lem7  30435  clsun  30984  mblfinlem3  31979  ismblfin  31981  paddssat  33379  pclunN  33463  paddunN  33492  poldmj1N  33493  pclfinclN  33515  lsmfgcl  35932  ssuncl  36174  sssymdifcl  36176  undmrnresiss  36210  mptrcllem  36220  cnvrcl0  36232  dfrtrcl5  36236  brtrclfv2  36319  unhe1  36381  dffrege76  36535  iunopeqop  39005