Theorem unss 3530

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 3345	. 2 |- ( ( A u. B ) C_ C <-> A. x ( x e. ( A u. B ) -> x e. C ) )
2		19.26 1647	. . 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 3497	. . . . . 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 1610	. . 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 3345	. . . 4 |- ( A C_ C <-> A. x ( x e. A -> x e. C ) )
9		dfss2 3345	. . . 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 1367   e. wcel 1756   u. cun 3326   C_ wss 3328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-in 3335  df-ss 3342

This theorem is referenced by:  unssi  3531  unssd  3532  unssad  3533  unssbd  3534  nsspssun  3583  uneqin  3601  uneqdifeq  3767  prss  4027  prssg  4028  ssunsn2  4032  tpss  4038  pwundif  4628  eqrelrel  4941  xpsspw  4953  xpsspwOLD  4954  relun  4956  relcoi2  5365  fnsuppresOLD  5938  fnsuppres  6716  dfer2  7102  isinf  7526  fiin  7672  trcl  7948  supxrun  11278  isumltss  13311  rpnnen2  13508  lubun  15293  isipodrs  15331  fpwipodrs  15334  ipodrsima  15335  aspval2  17417  unocv  18105  uncld  18645  restntr  18786  cmpcld  19005  uncmp  19006  ufprim  19482  tsmsfbas  19698  ovolctb2  20975  ovolun  20982  unmbl  21019  plyun0  21665  sshjcl  24758  sshjval2  24814  shlub  24817  ssjo  24850  spanuni  24947  dfon2lem3  27598  dfon2lem7  27602  wfrlem15  27738  mblfinlem3  28430  ismblfin  28432  clsun  28523  lsmfgcl  29427  paddssat  33458  pclunN  33542  paddunN  33571  poldmj1N  33572  pclfinclN  33594