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

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

Proof of Theorem elun1
StepHypRef Expression
1 ssun1 4147 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3962 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  cun 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951
This theorem is referenced by:  brtpos  7900  dftpos4  7910  domunsncan  8616  unxpdomlem2  8722  rankunb  9278  rankelun  9300  djulcl  9338  djuss  9348  djuun  9354  fin1a2lem10  9830  zornn0g  9926  xrsupexmnf  12697  xrinfmexpnf  12698  sumsplit  15122  lcmfunsnlem2lem1  15981  lcmfunsnlem2  15983  prmreclem5  16255  smndex1mnd  18074  smndex1id  18075  lbsextlem3  19931  restntr  21789  comppfsc  22139  1stckgenlem  22160  fbun  22447  filconn  22490  filuni  22492  alexsubALTlem4  22657  ovolfiniun  24101  volfiniun  24147  elplyd  24791  ply1term  24793  aannenlem2  24917  aalioulem2  24921  eengbas  26766  ecgrtg  26768  gsumle  30725  reprsuc  31886  bnj1498  32333  mrsubcn  32766  mrsubco  32768  altxpsspw  33438  matunitlindflem1  34887  poimirlem9  34900  poimirlem22  34913  poimirlem31  34922  poimirlem32  34923  mbfresfi  34937  itg2addnclem2  34943  ftc1anclem7  34972  ftc1anc  34974  hdmaplem1  38906  hdmap1eulem  38957  sucidALTVD  41204  sucidALT  41205  founiiun0  41451  mccllem  41878  limcresiooub  41923  limcresioolb  41924  cnrefiisplem  42110  dvmptfprodlem  42229  dvnprodlem2  42232  fourierdlem48  42440  fourierdlem49  42441  fourierdlem51  42443  fourierdlem54  42446  fourierdlem62  42454  fourierdlem71  42463  fourierdlem103  42495  fourierdlem104  42496  fourierdlem114  42506  fouriersw  42517  nnfoctbdjlem  42738  hoidmvlelem2  42879  hoidmvlelem3  42880  pimrecltpos  42988  setsnidel  43538
  Copyright terms: Public domain W3C validator