Theorem elssuni 4192

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 3436	. 2 |- A C_ A
2		ssuni 4185	. 2 |- ( ( A C_ A /\ A e. B ) -> A C_ U. B )
3	1, 2	mpan 668	1 |- ( A e. B -> A C_ U. B )

Syntax hints:   -> wi 4   e. wcel 1826   C_ wss 3389   U.cuni 4163

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-in 3396  df-ss 3403  df-uni 4164

This theorem is referenced by:  unissel  4193  ssunieq  4197  pwuni  4593  pwel  4614  uniopel  4665  dmrnssfld  5174  unixp0  5450  fvssunirn  5797  sorpssuni  6488  iunpw  6513  pwuninel2  6921  onfununi  6930  tfrlem9  6972  tfrlem9a  6973  tfrlem13  6977  sbthlem1  7546  sbthlem2  7547  2pwuninel  7591  ordunifi  7685  unifpw  7738  fissuni  7740  dffi3  7806  cantnfp1lem3  8012  oemapvali  8016  cantnflem1  8021  cantnfp1lem3OLD  8038  cantnflem1OLD  8044  cnfcom3lem  8060  cnfcom3lemOLD  8068  rankuni2b  8184  carduni  8275  r0weon  8303  dfac8clem  8326  cardinfima  8391  alephfp  8402  iunfictbso  8408  dfac5lem4  8420  dfac2a  8423  dfacacn  8434  dfac12lem2  8437  kmlem2  8444  fin23lem16  8628  fin23lem21  8632  isf32lem5  8650  fin1a2lem11  8703  fin1a2lem13  8705  itunitc  8714  axdc2lem  8741  axdc3lem2  8744  ttukeylem5  8806  ttukeylem6  8807  fpwwe2lem11  8929  fpwwe2lem12  8930  fpwwe2lem13  8931  fpwwe2  8932  wunex2  9027  inatsk  9067  tskuni  9072  suplem1pr  9341  suplem2pr  9342  unirnioo  11545  mrcuni  15028  isacs3lem  15913  mrelatlub  15933  dprd2dlem1  17203  lbsextlem2  17918  eltopss  19501  toponss  19515  isbasis3g  19535  baspartn  19540  bastg  19552  tgcl  19556  fctop  19590  cctop  19592  ppttop  19593  epttop  19595  difopn  19620  ssntr  19644  isopn3  19653  isopn3i  19669  toponmre  19680  neiuni  19709  neiptoptop  19718  resttopon  19748  restopn2  19764  perfopn  19772  pnfnei  19807  mnfnei  19808  ssidcn  19842  lmcnp  19891  pnrmopn  19930  ist1-2  19934  nrmsep  19944  isnrm2  19945  isnrm3  19946  regsep2  19963  cncmp  19978  hauscmplem  19992  hauscmp  19993  conndisj  20002  cnconn  20008  concompss  20019  islly2  20070  nllyrest  20072  nllyidm  20075  hausllycmp  20080  cldllycmp  20081  lly1stc  20082  comppfsc  20118  kgentopon  20124  kgenss  20129  llycmpkgen2  20136  1stckgen  20140  txuni2  20151  ptpjpre1  20157  ptuni2  20162  ptbasfi  20167  xkouni  20185  txcnpi  20194  ptpjopn  20198  txindis  20220  txnlly  20223  txtube  20226  hausdiag  20231  xkopt  20241  xkococnlem  20245  txcon  20275  qtopuni  20288  qtopkgen  20296  tgqtop  20298  regr1lem  20325  kqreglem1  20327  kqreglem2  20328  kqnrmlem1  20329  kqnrmlem2  20330  hmeoimaf1o  20356  reghmph  20379  nrmhmph  20380  filcon  20469  trfil1  20472  ufildr  20517  flimfil  20555  flimfnfcls  20614  alexsublem  20629  alexsubALTlem3  20634  ustbas2  20813  tgioo  21386  xrtgioo  21396  xrsmopn  21402  opnreen  21421  cnheibor  21540  cnllycmp  21541  lebnumlem1  21546  lebnumlem3  21548  bcthlem5  21852  bcth3  21855  voliunlem1  22045  voliunlem3  22047  volsup  22051  opnmbllem  22095  mbfimaopnlem  22147  lhop  22502  tglnpt  24056  tglineintmo  24142  ubthlem1  25903  shatomistici  27396  hatomistici  27397  unifi3  27677  tpr2rico  28048  hasheuni  28233  difelsiga  28282  prob01  28535  probdsb  28544  totprobd  28548  probmeasb  28552  cndprobtot  28558  orvcelval  28590  pconcon  28865  cvmsf1o  28906  cvmscld  28907  cvmsss2  28908  cvmopnlem  28912  cvmfolem  28913  cvmliftmolem1  28915  cvmliftlem6  28924  cvmliftlem8  28926  cvmlift2lem9  28945  cvmlift2lem11  28947  cvmlift2lem12  28948  cvmlift3lem6  28958  dfon2lem3  29382  dfon2lem7  29386  trpredpred  29476  wfrlem12  29519  wfrlem16  29523  frrlem11  29564  nobndlem2  29618  nobndlem8  29624  nofulllem3  29629  nofulllem5  29631  opnmbllem0  30215  mbfresfi  30226  ntruni  30311  clsint2  30313  neibastop1  30343  topmeet  30348  topjoin  30349  fnemeet1  30350  fnejoin1  30352  heiborlem1  30473  isnacs3  30808  aomclem4  31169  kelac2  31177  stoweidlem28  31976  stoweidlem50  31998  stoweidlem52  32000  stoweidlem53  32001  stoweidlem54  32002  bnj1450  34453  bnj1501  34470  lssats  35150  dicval  37316  mapdunirnN  37790