MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elun2 Structured version   Visualization version   GIF version

Theorem elun2 3779
Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
elun2 (𝐴𝐵𝐴 ∈ (𝐶𝐵))

Proof of Theorem elun2
StepHypRef Expression
1 ssun2 3775 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3597 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1989  cun 3570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-in 3579  df-ss 3586
This theorem is referenced by:  dftpos4  7368  wfrlem14  7425  tfrlem11  7481  findcard2d  8199  cantnfp1lem1  8572  cantnfp1lem3  8574  tc2  8615  rankunb  8710  rankelun  8732  dfac2  8950  cfsmolem  9089  isfin4-3  9134  zornn0g  9324  mnfxr  10093  supxrun  12143  fsumsplitsnun  14478  fsumsplitsnunOLD  14480  sumsplit  14493  modfsummodslem1  14518  prmreclem5  15618  acsfiindd  17171  lspsolv  19137  mplcoe1  19459  maducoeval2  20440  restntr  20980  1stckgenlem  21350  fbun  21638  filuni  21683  ufileu  21717  alexsubALTlem4  21848  tmdgsum  21893  icccmplem2  22620  aannenlem2  24078  aalioulem2  24082  ebtwntg  25856  elntg  25858  bnj553  30953  bnj966  30999  bnj1442  31102  mrsubrn  31395  elmrsubrn  31402  mvhf  31440  msubvrs  31442  altxpsspw  32068  matunitlindflem1  33385  poimirlem3  33392  poimirlem31  33420  poimirlem32  33421  mbfresfi  33436  itg2addnclem2  33442  ftc1anclem7  33471  ftc1anc  33473  hdmaplem2N  36887  hdmaplem3  36888  sucidVD  38934  mccllem  39635  limcresiooub  39680  limcresioolb  39681  dvmptfprodlem  39928  dvmptfprod  39929  dvnprodlem1  39930  dvnprodlem2  39931  fourierdlem20  40113  fourierdlem38  40131  fourierdlem48  40140  fourierdlem49  40141  fourierdlem51  40143  fourierdlem62  40154  fourierdlem63  40155  fourierdlem64  40156  fourierdlem65  40157  fourierdlem71  40163  fouriersw  40217  nnfoctbdjlem  40441  isomenndlem  40513  hoiprodp1  40571  hoidmvlelem1  40578  hoidmvlelem2  40579  hoidmvlelem3  40580  hoidmvlelem4  40581  hspmbllem2  40610  pimrecltpos  40688  setsidel  41116
  Copyright terms: Public domain W3C validator