Theorem unss 3663

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 3478	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1667	. . 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 3630	. . . . . 6 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	imbi1i 325	. . . . 5 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A \/ x e. B ) -> x e. C ) )
5		jaob 783	. . . . 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 249	. . . 4 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A -> x e. C ) /\ ( x e. B -> x e. C ) ) )
7	6	albii 1627	. . 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 3478	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3478	. . . 4 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
10	8, 9	anbi12i 697	. . 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 277	. 2 |- ( A. x ( x e. ( A u. B ) -> x e. C ) <-> ( A C_ C /\ B C_ C ) )
12	1, 11	bitr2i 250	1 |- ( ( A C_ C /\ B C_ C ) <-> ( A u. B ) C_ C )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   A.wal 1381   e. wcel 1804   u. cun 3459   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475

This theorem is referenced by:  unssi  3664  unssd  3665  unssad  3666  unssbd  3667  nsspssun  3716  uneqin  3734  uneqdifeq  3902  prss  4169  prssg  4170  ssunsn2  4174  tpss  4180  pwundif  4777  eqrelrel  5094  xpsspw  5106  xpsspwOLD  5107  relun  5109  relcoi2  5525  fnsuppresOLD  6116  fnsuppres  6929  dfer2  7314  isinf  7735  fiin  7884  trcl  8162  supxrun  11518  isumltss  13642  rpnnen2  13941  lubun  15732  isipodrs  15770  fpwipodrs  15773  ipodrsima  15774  aspval2  17975  unocv  18689  uncld  19520  restntr  19661  cmpcld  19880  uncmp  19881  ufprim  20388  tsmsfbas  20604  ovolctb2  21881  ovolun  21888  unmbl  21926  plyun0  22572  sshjcl  26251  sshjval2  26307  shlub  26310  ssjo  26343  spanuni  26440  dfon2lem3  29193  dfon2lem7  29197  wfrlem15  29333  mblfinlem3  30029  ismblfin  30031  clsun  30122  lsmfgcl  30996  paddssat  35413  pclunN  35497  paddunN  35526  poldmj1N  35527  pclfinclN  35549  ssuncl  37593  sssymdifcl  37595  unhe1  37630