Theorem unss 3678

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 3493	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1657	. . 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 3645	. . . . . 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 781	. . . . 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 1620	. . 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 3493	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3493	. . . 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 1377   e. wcel 1767   u. cun 3474   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490

This theorem is referenced by:  unssi  3679  unssd  3680  unssad  3681  unssbd  3682  nsspssun  3731  uneqin  3749  uneqdifeq  3915  prss  4181  prssg  4182  ssunsn2  4186  tpss  4192  pwundif  4787  eqrelrel  5103  xpsspw  5115  xpsspwOLD  5116  relun  5118  relcoi2  5534  fnsuppresOLD  6120  fnsuppres  6927  dfer2  7312  isinf  7733  fiin  7881  trcl  8158  supxrun  11506  isumltss  13622  rpnnen2  13819  lubun  15609  isipodrs  15647  fpwipodrs  15650  ipodrsima  15651  aspval2  17783  unocv  18494  uncld  19324  restntr  19465  cmpcld  19684  uncmp  19685  ufprim  20161  tsmsfbas  20377  ovolctb2  21654  ovolun  21661  unmbl  21699  plyun0  22345  sshjcl  25965  sshjval2  26021  shlub  26024  ssjo  26057  spanuni  26154  fcoinver  27149  dfon2lem3  28810  dfon2lem7  28814  wfrlem15  28950  mblfinlem3  29646  ismblfin  29648  clsun  29739  lsmfgcl  30640  icccncfext  31242  cncfiooicclem1  31248  fourierdlem62  31485  fourierdlem101  31524  paddssat  34619  pclunN  34703  paddunN  34732  poldmj1N  34733  pclfinclN  34755  ssuncl  36784  sssymdifcl  36786