Theorem unss 3599

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 3407	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1740	. . 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 3565	. . . . . 6 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	imbi1i 332	. . . . 5 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A \/ x e. B ) -> x e. C ) )
5		jaob 800	. . . . 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 257	. . . 4 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
7	6	albii 1699	. . 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 3407	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3407	. . . 4 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
10	8, 9	anbi12i 711	. . 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 285	. 2 |- ( A. x ( x e. ( A u. B ) -> x e. C ) <-> ( A C_ C /\ B C_ C ) )
12	1, 11	bitr2i 258	1 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )

Syntax hints:   -> wi 4   <-> wb 189   \/ wo 375   /\ wa 376   A.wal 1450   e. wcel 1904   u. cun 3388   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-in 3397  df-ss 3404

This theorem is referenced by:  unssi  3600  unssd  3601  unssad  3602  unssbd  3603  nsspssun  3667  uneqin  3685  uneqdifeq  3847  prss  4117  prssg  4118  ssunsn2  4123  tpss  4129  pwundif  4746  eqrelrel  4941  xpsspw  4953  relun  4955  relcoi2  5370  fnsuppres  6961  wfrlem15  7068  dfer2  7382  isinf  7803  fiin  7954  trcl  8230  supxrun  11626  trclun  13155  isumltss  13983  rpnnen2  14355  lcmfunsnlem  14693  lcmfun  14697  coprmprod  14757  coprmproddvdslem  14758  lubun  16447  isipodrs  16485  fpwipodrs  16488  ipodrsima  16489  aspval2  18648  unocv  19320  uncld  20133  restntr  20275  cmpcld  20494  uncmp  20495  ufprim  21002  tsmsfbas  21220  ovolctb2  22523  ovolun  22530  unmbl  22569  plyun0  23230  sshjcl  27089  sshjval2  27145  shlub  27148  ssjo  27181  spanuni  27278  dfon2lem3  30502  dfon2lem7  30506  clsun  31055  mblfinlem3  32043  ismblfin  32045  paddssat  33450  pclunN  33534  paddunN  33563  poldmj1N  33564  pclfinclN  33586  lsmfgcl  36003  ssuncl  36245  sssymdifcl  36247  undmrnresiss  36281  mptrcllem  36291  cnvrcl0  36303  dfrtrcl5  36307  brtrclfv2  36390  unhe1  36452  dffrege76  36606  iunopeqop  39151