Theorem elssuni 2516

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.

Assertion

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

Proof of Theorem elssuni

Step	Hyp	Ref	Expression
1		ssid 2070	. 2 |- A (_ A
2		ssuni 2512	. 2 |- ((A (_ A /\ A e. B) -> A (_ U.B)
3	1, 2	mpan 693	1 |- (A e. B -> A (_ U.B)

Syntax hints:   -> wi 3   e. wcel 955   (_ wss 2037  U.cuni 2493

This theorem is referenced by:  unissel 2517  ssunieq 2521  pwuni 2747  pwel 2749  uniopel 2798  iunpw 2904  dmrnssfld 3343  tfrlem9 3904  tfrlem13 3908  sbthlem1 4427  sbthlem2 4428  2pwuninel 4465  pwuninelg 4467  rankuni2 4662  kmlem2 4738  carduni 4830  cardprc 4833  cardinfima 4863  alephfp 4872  suplem2pr 5134  unirnioo 6335  eltopss 7545  isbasis3g 7555  tgclt 7566  tgss2t 7579  bastop 7584  fctop 7592  cctop 7594  cncnplem4 7716  uniopn 7801  tgioo 7854  shatomistic 10196  hatomistic 10197  idhme 10409  hmphre 10417  homcard 10426  filintf 10443  dtopcl 10459

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-in 2041  df-ss 2043  df-uni 2494

Copyright terms: Public domain