Theorem elssuni 2526

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 2080	. 2 |- A (_ A
2		ssuni 2522	. 2 |- ((A (_ A /\ A e. B) -> A (_ U.B)
3	1, 2	mpan 695	1 |- (A e. B -> A (_ U.B)

Syntax hints:   -> wi 3   e. wcel 958   (_ wss 2047  U.cuni 2503

This theorem is referenced by:  unissel 2527  ssunieq 2531  pwuni 2757  pwel 2759  uniopel 2809  iunpw 2914  dmrnssfld 3357  tfrlem9 3919  tfrlem13 3923  sbthlem1 4447  sbthlem2 4448  pwuninel 4486  2pwuninel 4487  rankuni2 4690  kmlem2 4766  carduni 4858  cardprc 4861  cardinfima 4891  alephfp 4900  suplem2pr 5162  unirnioo 6402  eltopss 7603  isbasis3g 7613  tgclt 7624  tgss2t 7637  bastop 7642  fctopOLD 7650  cctop 7652  cncnplem4 7777  uniopn 7861  tgioo 7915  shatomistic 10288  hatomistic 10289  idhme 10522  hmphre 10530  homcard 10539  filintf 10569  dtopcl 10615

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051  df-ss 2053  df-uni 2504

Copyright terms: Public domain