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

Theorem elun1 4137
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 4133 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3941 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cun 3909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-un 3916  df-in 3918  df-ss 3928
This theorem is referenced by:  brtpos  8167  dftpos4  8177  domunsncan  9017  unxpdomlem2  9196  rankunb  9787  rankelun  9809  djulcl  9847  djuss  9857  djuun  9863  fin1a2lem10  10346  zornn0g  10442  xrsupexmnf  13225  xrinfmexpnf  13226  sumsplit  15654  lcmfunsnlem2lem1  16515  lcmfunsnlem2  16517  prmreclem5  16793  smndex1mnd  18721  smndex1id  18722  lbsextlem3  20624  restntr  22536  comppfsc  22886  1stckgenlem  22907  fbun  23194  filconn  23237  filuni  23239  alexsubALTlem4  23404  ovolfiniun  24868  volfiniun  24914  elplyd  25566  ply1term  25568  aannenlem2  25692  aalioulem2  25696  addsval  27277  addsid1  27279  addscom  27281  addsproplem2  27285  addsproplem6  27289  sleadd1  27301  addsass  27316  negsproplem2  27330  negsproplem6  27334  negsid  27342  eengbas  27933  ecgrtg  27935  gsumle  31935  reprsuc  33231  bnj1498  33676  mrsubcn  34116  mrsubco  34118  mulsval  34411  mulsid1  34414  mulsid2  34415  altxpsspw  34565  matunitlindflem1  36077  poimirlem9  36090  poimirlem22  36103  poimirlem31  36112  poimirlem32  36113  mbfresfi  36127  itg2addnclem2  36133  ftc1anclem7  36160  ftc1anc  36162  hdmaplem1  40237  hdmap1eulem  40288  metakunt21  40600  sucidALTVD  43159  sucidALT  43160  founiiun0  43416  pimxrneun  43731  mccllem  43845  limcresiooub  43890  limcresioolb  43891  cnrefiisplem  44077  dvmptfprodlem  44192  dvnprodlem2  44195  fourierdlem48  44402  fourierdlem49  44403  fourierdlem51  44405  fourierdlem54  44408  fourierdlem62  44416  fourierdlem71  44425  fourierdlem103  44457  fourierdlem104  44458  fourierdlem114  44468  fouriersw  44479  nnfoctbdjlem  44703  hoidmvlelem2  44844  hoidmvlelem3  44845  pimrecltpos  44956  setsnidel  45576
  Copyright terms: Public domain W3C validator