Theorem elssuni 2521

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

Syntax hints:   -> wi 3   e. wcel 956   (_ wss 2043  U.cuni 2498

This theorem is referenced by:  unissel 2522  ssunieq 2526  pwuni 2752  pwel 2754  uniopel 2804  iunpw 2909  dmrnssfld 3351  tfrlem9 3910  tfrlem13 3914  sbthlem1 4433  sbthlem2 4434  pwuninel 4472  2pwuninel 4473  rankuni2 4670  kmlem2 4746  carduni 4838  cardprc 4841  cardinfima 4871  alephfp 4880  suplem2pr 5142  unirnioo 6343  eltopss 7553  isbasis3g 7563  tgclt 7574  tgss2t 7587  bastop 7592  fctop 7600  cctop 7602  cncnplem4 7727  uniopn 7813  tgioo 7867  shatomistic 10225  hatomistic 10226  idhme 10445  hmphre 10453  homcard 10462  filintf 10479  dtopcl 10495

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-uni 2499

Copyright terms: Public domain