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

Theorem elun2 3765
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 3761 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3584 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cun 3558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-un 3565  df-in 3567  df-ss 3574
This theorem is referenced by:  dftpos4  7331  wfrlem14  7388  tfrlem11  7444  findcard2d  8162  cantnfp1lem1  8535  cantnfp1lem3  8537  tc2  8578  rankunb  8673  rankelun  8695  dfac2  8913  cfsmolem  9052  isfin4-3  9097  zornn0g  9287  mnfxr  10056  supxrun  12105  fsumsplitsnun  14433  sumsplit  14446  modfsummodslem1  14470  prmreclem5  15567  acsfiindd  17117  lspsolv  19083  mplcoe1  19405  maducoeval2  20386  restntr  20926  1stckgenlem  21296  fbun  21584  filuni  21629  ufileu  21663  alexsubALTlem4  21794  tmdgsum  21839  icccmplem2  22566  aannenlem2  24022  aalioulem2  24026  ebtwntg  25796  elntg  25798  bnj553  30729  bnj966  30775  bnj1442  30878  mrsubrn  31171  elmrsubrn  31178  mvhf  31216  msubvrs  31218  altxpsspw  31779  matunitlindflem1  33076  poimirlem3  33083  poimirlem31  33111  poimirlem32  33112  mbfresfi  33127  itg2addnclem2  33133  ftc1anclem7  33162  ftc1anc  33164  hdmaplem2N  36580  hdmaplem3  36581  sucidVD  38630  mccllem  39265  limcresiooub  39310  limcresioolb  39311  dvmptfprodlem  39496  dvmptfprod  39497  dvnprodlem1  39498  dvnprodlem2  39499  fourierdlem20  39681  fourierdlem38  39699  fourierdlem48  39708  fourierdlem49  39709  fourierdlem51  39711  fourierdlem62  39722  fourierdlem63  39723  fourierdlem64  39724  fourierdlem65  39725  fourierdlem71  39731  fouriersw  39785  nnfoctbdjlem  40009  isomenndlem  40081  hoiprodp1  40139  hoidmvlelem1  40146  hoidmvlelem2  40147  hoidmvlelem3  40148  hoidmvlelem4  40149  hspmbllem2  40178  pimrecltpos  40256  setsidel  40674
  Copyright terms: Public domain W3C validator