Theorem elssuni 4467

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. (Contributed by NM, 6-Jun-1994.)

Assertion

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

Proof of Theorem elssuni

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

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-uni 4437

This theorem is referenced by:  unissel  4468  ssunieq  4472  pwuni  4474  pwel  4920  uniopel  4978  dmrnssfld  5384  unixp0  5669  fvssunirn  6217  sorpssuni  6946  iunpw  6978  pwuninel2  7400  wfrlem12  7426  wfrlem16  7430  wfrlem17  7431  onfununi  7438  tfrlem9  7481  tfrlem9a  7482  tfrlem13  7486  sbthlem1  8070  sbthlem2  8071  2pwuninel  8115  ordunifi  8210  unifpw  8269  fissuni  8271  dffi3  8337  cantnfp1lem3  8577  oemapvali  8581  cantnflem1  8586  cnfcom3lem  8600  rankuni2b  8716  carduni  8807  r0weon  8835  dfac8clem  8855  cardinfima  8920  alephfp  8931  iunfictbso  8937  dfac5lem4  8949  dfac2a  8952  dfacacn  8963  dfac12lem2  8966  kmlem2  8973  fin23lem16  9157  fin23lem21  9161  isf32lem5  9179  fin1a2lem11  9232  fin1a2lem13  9234  itunitc  9243  axdc2lem  9270  axdc3lem2  9273  ttukeylem5  9335  ttukeylem6  9336  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  wunex2  9560  inatsk  9600  tskuni  9605  suplem1pr  9874  suplem2pr  9875  unirnioo  12273  mrcuni  16281  isacs3lem  17166  mrelatlub  17186  dprd2dlem1  18440  lbsextlem2  19159  eltopss  20712  toponss  20731  isbasis3g  20753  baspartn  20758  bastg  20770  tgcl  20773  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  difopn  20838  ssntr  20862  isopn3  20870  isopn3i  20886  toponmre  20897  neiuni  20926  neiptoptop  20935  resttopon  20965  restopn2  20981  perfopn  20989  pnfnei  21024  mnfnei  21025  ssidcn  21059  lmcnp  21108  pnrmopn  21147  ist1-2  21151  nrmsep  21161  isnrm2  21162  isnrm3  21163  regsep2  21180  cncmp  21195  hauscmplem  21209  hauscmp  21210  conndisj  21219  cnconn  21225  conncompss  21236  islly2  21287  nllyrest  21289  nllyidm  21292  hausllycmp  21297  cldllycmp  21298  lly1stc  21299  comppfsc  21335  kgentopon  21341  kgenss  21346  llycmpkgen2  21353  1stckgen  21357  txuni2  21368  ptpjpre1  21374  ptuni2  21379  ptbasfi  21384  xkouni  21402  txcnpi  21411  ptpjopn  21415  txindis  21437  txnlly  21440  txtube  21443  hausdiag  21448  xkopt  21458  xkococnlem  21462  txconn  21492  qtopuni  21505  qtopkgen  21513  tgqtop  21515  regr1lem  21542  kqreglem1  21544  kqreglem2  21545  kqnrmlem1  21546  kqnrmlem2  21547  hmeoimaf1o  21573  reghmph  21596  nrmhmph  21597  filconn  21687  trfil1  21690  ufildr  21735  flimfil  21773  flimfnfcls  21832  alexsublem  21848  alexsubALTlem3  21853  ustbas2  22029  tgioo  22599  xrtgioo  22609  xrsmopn  22615  opnreen  22634  cnheibor  22754  cnllycmp  22755  lebnumlem1  22760  lebnumlem3  22762  bcthlem5  23125  bcth3  23128  voliunlem1  23318  voliunlem3  23320  volsup  23324  opnmbllem  23369  mbfimaopnlem  23422  lhop  23779  tglnpt  25444  tglineintmo  25537  ubthlem1  27726  shatomistici  29220  hatomistici  29221  unifi3  29490  tpr2rico  29958  hasheuni  30147  difelsiga  30196  prob01  30475  probdsb  30484  totprobd  30488  probmeasb  30492  cndprobtot  30498  orvcelval  30530  bnj1450  31118  bnj1501  31135  pconnconn  31213  cvmsf1o  31254  cvmscld  31255  cvmsss2  31256  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem1  31263  cvmliftlem6  31272  cvmliftlem8  31274  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift2lem12  31296  cvmlift3lem6  31306  dfon2lem3  31690  dfon2lem7  31694  trpredpred  31728  frrlem11  31792  nosupno  31849  nosupbday  31851  noetalem3  31865  ntruni  32322  clsint2  32324  neibastop1  32354  topmeet  32359  topjoin  32360  fnemeet1  32361  fnejoin1  32363  opnmbllem0  33445  mbfresfi  33456  heiborlem1  33610  lssats  34299  dicval  36465  mapdunirnN  36939  isnacs3  37273  aomclem4  37627  kelac2  37635  ssuniint  39250  stoweidlem28  40245  stoweidlem50  40267  stoweidlem52  40269  stoweidlem53  40270  stoweidlem54  40271  prsal  40538  salincl  40543  saliincl  40545  saldifcl2  40546  salexct  40552  psmeasurelem  40687  caragenuni  40725  carageniuncl  40737  caratheodorylem1  40740  caratheodorylem2  40741  voncmpl  40835  setrec1lem2  42435  setrec2fun  42439