Theorem elssuni 3206

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 C_ U.B)

Proof of Theorem elssuni

Step	Hyp	Ref	Expression
1		ssid 2634	. 2 |- A C_ A
2		ssuni 3201	. 2 |- ((A C_ A /\ A e. B) -> A C_ U.B)
3	1, 2	mpan 759	1 |- (A e. B -> A C_ U.B)

Syntax hints:   -> wi 3   e. wcel 1300   C_ wss 2593  U.cuni 3177

This theorem is referenced by:  unissel 3207  ssunieq 3211  pwuni 3505  pwel 3506  uniopel 3556  iunpw 3858  dmrnssfld 4205  onfununi 5116  tfrlem9 5127  tfrlem13 5131  sbthlem1 5510  sbthlem2 5511  pwuninel 5550  2pwuninel 5551  rankuni2 5801  kmlem2 5928  carduni 6010  cardprc 6013  cardinfima 6039  alephfp 6048  suplem2pr 6314  unirnioo 7571  eltopss 8872  isbasis3g 8882  tgcl 8894  tgss2 8907  bastop1 8912  fctop 8920  cctop 8922  txuni 8935  cncnplem4 9054  uniopn2 9138  tgioo 9193  filintf 10274  fbssfg 10285  fgfil 10290  extbas1 10291  filrn 10293  isflimf 10323  cncomp 10331  usinuniop 10341  shatomistici 11933  hatomistici 11934  bnj1515 13174  bnj1450 13541  dfon2lem3 13851  dfon2lem7 13855  trclpred 13934  wfrlem12 13968  wfrlem16 13972  axfelem1 14031  axfelem10 14040  axfelem15 14045  unint2t 14866  intfmu2 14867  osneisi 14875  idhme 14879  hmphre 14884  homcard 14893  conttnf 14944  dtopcl 14948  lvsovso 15038  lvsovso3 15040  opncldf1 15402  ssntr 15405  ntruni 15412  clsint2 15414  alexsublem3 15439  isfne3 15482  topfneec 15501  neibastop1 15518  neibastop2 15523  neibastop3 15524  topmtcl 15525  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin1 15530  fnejoin2 15531  neifg 15559  supfil 15560  isufil2 15565  filssufillem 15570  ufileulem 15572  ufileu 15573  filufint 15574  uffixfr 15575  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  rnelfm 15593  fmfnfmlem4 15597  fmfnfm 15598  filfm 15600  isfclus 15606  flimfnfcls 15615  fcluscomplem 15620  fcluscomp 15621  filnet 15645  heiborlem23 15977

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178

Copyright terms: Public domain