Theorem elssuni 3892

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 3221	. 2 |- A C_ A
2		ssuni 3886	. 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 2178   C_ wss 3174   U.cuni 3864

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-in 3180  df-ss 3187  df-uni 3865

This theorem is referenced by:  unissel  3893  ssunieq  3897  pwuni  4252  pwel  4280  uniopel  4319  iunpw  4545  dmrnssfld  4960  iotaexab  5269  fvssunirng  5614  relfvssunirn  5615  sefvex  5620  riotaexg  5926  pwuninel2  6391  tfrlem9  6428  tfrexlem  6443  sbthlem1  7085  sbthlem2  7086  unirnioo  10130  eltopss  14596  toponss  14613  isbasis3g  14633  baspartn  14637  bastg  14648  tgcl  14651  epttop  14677  difopn  14695  ssntr  14709  isopn3  14712  isopn3i  14722  neiuni  14748  resttopon  14758  restopn2  14770  ssidcn  14797  lmtopcnp  14837  txuni2  14843  hmeoimaf1o  14901  tgioo  15141  bj-elssuniab  15927