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

Theorem elun1 3741
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 3737 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3563 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553
This theorem is referenced by:  brtpos  7225  dftpos4  7235  domunsncan  7922  unxpdomlem2  8027  rankunb  8573  rankelun  8595  fin1a2lem10  9091  zornn0g  9187  xrsupexmnf  11963  xrinfmexpnf  11964  sumsplit  14287  lcmfunsnlem2lem1  15135  lcmfunsnlem2  15137  prmreclem5  15408  lbsextlem3  18927  restntr  20738  comppfsc  21087  1stckgenlem  21108  fbun  21396  filcon  21439  filuni  21441  alexsubALTlem4  21606  ovolfiniun  22993  volfiniun  23039  elplyd  23679  ply1term  23681  aannenlem2  23805  aalioulem2  23809  eengbas  25579  ecgrtg  25581  vdgrf  26191  gsumle  28916  bnj1498  30189  mrsubcn  30476  mrsubco  30478  altxpsspw  31060  matunitlindflem1  32371  poimirlem9  32384  poimirlem22  32397  poimirlem31  32406  poimirlem32  32407  mbfresfi  32422  itg2addnclem2  32428  ftc1anclem7  32457  ftc1anc  32459  hdmaplem1  35874  hdmap1eulem  35927  sucidALTVD  37924  sucidALT  37925  founiiun0  38168  mccllem  38461  limcresiooub  38506  limcresioolb  38507  dvmptfprodlem  38631  dvnprodlem2  38634  fourierdlem48  38844  fourierdlem49  38845  fourierdlem51  38847  fourierdlem54  38850  fourierdlem62  38858  fourierdlem71  38867  fourierdlem103  38899  fourierdlem104  38900  fourierdlem114  38910  fouriersw  38921  nnfoctbdjlem  39145  hoidmvlelem2  39283  hoidmvlelem3  39284  pimrecltpos  39393
  Copyright terms: Public domain W3C validator