Theorem unss 3616

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 3430	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1701	. . 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 3583	. . . . . 6 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	imbi1i 323	. . . . 5 |- ( ( x e. ( A u. B ) -> x e. C ) <-> ( ( x e. A \/ x e. B ) -> x e. C ) )
5		jaob 784	. . . . 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 1661	. . 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 3430	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3430	. . . 4 |- ( B C_ C <-> A. x ( x e. B -> x e. C ) )
10	8, 9	anbi12i 695	. . 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 366   /\ wa 367   A.wal 1403   e. wcel 1842   u. cun 3411   C_ wss 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-un 3418  df-in 3420  df-ss 3427

This theorem is referenced by:  unssi  3617  unssd  3618  unssad  3619  unssbd  3620  nsspssun  3682  uneqin  3700  uneqdifeq  3859  prss  4125  prssg  4126  ssunsn2  4130  tpss  4136  pwundif  4729  eqrelrel  4924  xpsspw  4936  relun  4938  relcoi2  5350  fnsuppresOLD  6112  fnsuppres  6929  wfrlem15  7034  dfer2  7348  isinf  7767  fiin  7915  trcl  8190  supxrun  11559  trclun  12995  isumltss  13809  rpnnen2  14166  lubun  16075  isipodrs  16113  fpwipodrs  16116  ipodrsima  16117  aspval2  18314  unocv  19007  uncld  19832  restntr  19974  cmpcld  20193  uncmp  20194  ufprim  20700  tsmsfbas  20916  ovolctb2  22193  ovolun  22200  unmbl  22238  plyun0  22884  sshjcl  26673  sshjval2  26729  shlub  26732  ssjo  26765  spanuni  26862  dfon2lem3  29991  dfon2lem7  29995  clsun  30543  mblfinlem3  31405  ismblfin  31407  paddssat  32811  pclunN  32895  paddunN  32924  poldmj1N  32925  pclfinclN  32947  lsmfgcl  35362  ssuncl  35601  sssymdifcl  35603  brtrclfv2  35686  unhe1  35746  dffrege76  35900