Theorem elssuni 2524

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 2078	. 2 |- A (_ A
2		ssuni 2520	. 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 2045  U.cuni 2501

This theorem is referenced by:  unissel 2525  ssunieq 2529  pwuni 2755  pwel 2757  uniopel 2807  iunpw 2912  dmrnssfld 3355  tfrlem9 3917  tfrlem13 3921  sbthlem1 4441  sbthlem2 4442  pwuninel 4480  2pwuninel 4481  rankuni2 4678  kmlem2 4754  carduni 4846  cardprc 4849  cardinfima 4879  alephfp 4888  suplem2pr 5150  unirnioo 6362  eltopss 7560  isbasis3g 7570  tgclt 7581  tgss2t 7594  bastop 7599  fctop 7607  cctop 7609  cncnplem4 7734  uniopn 7818  tgioo 7872  shatomistic 10243  hatomistic 10244  idhme 10464  hmphre 10472  homcard 10481  filintf 10498  dtopcl 10527

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 1810  df-in 2049  df-ss 2051  df-uni 2502

Copyright terms: Public domain