Theorem elssuni 3926

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 3248	. 2 |- A C_ A
2		ssuni 3920	. 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 2202   C_ wss 3201   U.cuni 3898

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-in 3207  df-ss 3214  df-uni 3899

This theorem is referenced by:  unissel  3927  ssunieq  3931  pwuni  4288  pwel  4316  uniopel  4355  iunpw  4583  dmrnssfld  5001  iotaexab  5312  fvssunirng  5663  relfvssunirn  5664  sefvex  5669  riotaexg  5985  pwuninel2  6491  tfrlem9  6528  tfrexlem  6543  sbthlem1  7199  sbthlem2  7200  unirnioo  10252  eltopss  14803  toponss  14820  isbasis3g  14840  baspartn  14844  bastg  14855  tgcl  14858  epttop  14884  difopn  14902  ssntr  14916  isopn3  14919  isopn3i  14929  neiuni  14955  resttopon  14965  restopn2  14977  ssidcn  15004  lmtopcnp  15044  txuni2  15050  hmeoimaf1o  15108  tgioo  15348  bj-elssuniab  16492