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

Theorem elun1 3921
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 3917 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3738 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2137  cun 3711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-un 3718  df-in 3720  df-ss 3727
This theorem is referenced by:  brtpos  7528  dftpos4  7538  domunsncan  8223  unxpdomlem2  8328  rankunb  8884  rankelun  8906  djulcl  8942  djuun  8948  fin1a2lem10  9421  zornn0g  9517  xrsupexmnf  12326  xrinfmexpnf  12327  sumsplit  14696  lcmfunsnlem2lem1  15551  lcmfunsnlem2  15553  prmreclem5  15824  lbsextlem3  19360  restntr  21186  comppfsc  21535  1stckgenlem  21556  fbun  21843  filconn  21886  filuni  21888  alexsubALTlem4  22053  ovolfiniun  23467  volfiniun  23513  elplyd  24155  ply1term  24157  aannenlem2  24281  aalioulem2  24285  eengbas  26058  ecgrtg  26060  gsumle  30086  reprsuc  31000  bnj1498  31434  mrsubcn  31721  mrsubco  31723  altxpsspw  32388  matunitlindflem1  33716  poimirlem9  33729  poimirlem22  33742  poimirlem31  33751  poimirlem32  33752  mbfresfi  33767  itg2addnclem2  33773  ftc1anclem7  33802  ftc1anc  33804  hdmaplem1  37560  hdmap1eulem  37613  sucidALTVD  39603  sucidALT  39604  founiiun0  39874  mccllem  40330  limcresiooub  40375  limcresioolb  40376  cnrefiisplem  40556  dvmptfprodlem  40660  dvnprodlem2  40663  fourierdlem48  40872  fourierdlem49  40873  fourierdlem51  40875  fourierdlem54  40878  fourierdlem62  40886  fourierdlem71  40895  fourierdlem103  40927  fourierdlem104  40928  fourierdlem114  40938  fouriersw  40949  nnfoctbdjlem  41173  hoidmvlelem2  41314  hoidmvlelem3  41315  pimrecltpos  41423  setsnidel  41855
  Copyright terms: Public domain W3C validator