Theorem elssuni 3877

Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
elssuni	|- ( A e. B -> A C_ U. B )

Proof of Theorem elssuni

Step	Hyp	Ref	Expression
1		ssid 3212	. 2 |- A C_ A
2		ssuni 3871	. 2 |- ( ( A C_ A /\ A e. B ) -> A C_ U. B )
3	1, 2	mpan 424	1 |- ( A e. B -> A C_ U. B )

Syntax hints:   -> wi 4   e. wcel 2175   C_ wss 3165   U.cuni 3849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-in 3171  df-ss 3178  df-uni 3850

This theorem is referenced by:  unissel  3878  ssunieq  3882  pwuni  4235  pwel  4261  uniopel  4300  iunpw  4526  dmrnssfld  4940  iotaexab  5249  fvssunirng  5590  relfvssunirn  5591  sefvex  5596  riotaexg  5902  pwuninel2  6367  tfrlem9  6404  tfrexlem  6419  sbthlem1  7058  sbthlem2  7059  unirnioo  10094  eltopss  14452  toponss  14469  isbasis3g  14489  baspartn  14493  bastg  14504  tgcl  14507  epttop  14533  difopn  14551  ssntr  14565  isopn3  14568  isopn3i  14578  neiuni  14604  resttopon  14614  restopn2  14626  ssidcn  14653  lmtopcnp  14693  txuni2  14699  hmeoimaf1o  14757  tgioo  14997  bj-elssuniab  15689