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

Theorem elun1 3742
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 3738 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3564 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cun 3538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554
This theorem is referenced by:  brtpos  7248  dftpos4  7258  domunsncan  7945  unxpdomlem2  8050  rankunb  8596  rankelun  8618  fin1a2lem10  9114  zornn0g  9210  xrsupexmnf  12007  xrinfmexpnf  12008  sumsplit  14341  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  prmreclem5  15462  lbsextlem3  18981  restntr  20796  comppfsc  21145  1stckgenlem  21166  fbun  21454  filcon  21497  filuni  21499  alexsubALTlem4  21664  ovolfiniun  23076  volfiniun  23122  elplyd  23762  ply1term  23764  aannenlem2  23888  aalioulem2  23892  eengbas  25661  ecgrtg  25663  vdgrf  26425  gsumle  29110  bnj1498  30383  mrsubcn  30670  mrsubco  30672  altxpsspw  31254  matunitlindflem1  32575  poimirlem9  32588  poimirlem22  32601  poimirlem31  32610  poimirlem32  32611  mbfresfi  32626  itg2addnclem2  32632  ftc1anclem7  32661  ftc1anc  32663  hdmaplem1  36078  hdmap1eulem  36131  sucidALTVD  38128  sucidALT  38129  founiiun0  38372  mccllem  38664  limcresiooub  38709  limcresioolb  38710  dvmptfprodlem  38834  dvnprodlem2  38837  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem62  39061  fourierdlem71  39070  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  fouriersw  39124  nnfoctbdjlem  39348  hoidmvlelem2  39486  hoidmvlelem3  39487  pimrecltpos  39596
  Copyright terms: Public domain W3C validator