Theorem elun1 4106

Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elun1	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 4102	. 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
2	1	sseli 3913	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2108   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  brtpos  8022  dftpos4  8032  domunsncan  8812  unxpdomlem2  8957  rankunb  9539  rankelun  9561  djulcl  9599  djuss  9609  djuun  9615  fin1a2lem10  10096  zornn0g  10192  xrsupexmnf  12968  xrinfmexpnf  12969  sumsplit  15408  lcmfunsnlem2lem1  16271  lcmfunsnlem2  16273  prmreclem5  16549  smndex1mnd  18464  smndex1id  18465  lbsextlem3  20337  restntr  22241  comppfsc  22591  1stckgenlem  22612  fbun  22899  filconn  22942  filuni  22944  alexsubALTlem4  23109  ovolfiniun  24570  volfiniun  24616  elplyd  25268  ply1term  25270  aannenlem2  25394  aalioulem2  25398  eengbas  27252  ecgrtg  27254  gsumle  31252  reprsuc  32495  bnj1498  32941  mrsubcn  33381  mrsubco  33383  addsval  34053  addsid1  34054  addscom  34056  altxpsspw  34206  matunitlindflem1  35700  poimirlem9  35713  poimirlem22  35726  poimirlem31  35735  poimirlem32  35736  mbfresfi  35750  itg2addnclem2  35756  ftc1anclem7  35783  ftc1anc  35785  hdmaplem1  39712  hdmap1eulem  39763  metakunt21  40073  sucidALTVD  42379  sucidALT  42380  founiiun0  42617  mccllem  43028  limcresiooub  43073  limcresioolb  43074  cnrefiisplem  43260  dvmptfprodlem  43375  dvnprodlem2  43378  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem54  43591  fourierdlem62  43599  fourierdlem71  43608  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  fouriersw  43662  nnfoctbdjlem  43883  hoidmvlelem2  44024  hoidmvlelem3  44025  pimrecltpos  44133  setsnidel  44717