Theorem elun1 4132

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 4128	. 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
2	1	sseli 3927	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2113   ∪ cun 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  resf1extb  7874  brtpos  8175  dftpos4  8185  domunsncan  9003  unxpdomlem2  9155  rankunb  9760  rankelun  9782  djulcl  9820  djuss  9830  djuun  9836  fin1a2lem10  10317  zornn0g  10413  xrsupexmnf  13218  xrinfmexpnf  13219  sumsplit  15689  lcmfunsnlem2lem1  16563  lcmfunsnlem2  16565  prmreclem5  16846  smndex1mnd  18833  smndex1id  18834  gsumle  20072  lbsextlem3  21113  restntr  23124  comppfsc  23474  1stckgenlem  23495  fbun  23782  filconn  23825  filuni  23827  alexsubALTlem4  23992  ovolfiniun  25456  volfiniun  25502  elplyd  26161  ply1term  26163  aannenlem2  26291  aalioulem2  26295  eqscut3  27792  cutlt  27903  addsval  27932  addsrid  27934  addscom  27936  addsproplem2  27940  addsproplem6  27944  sleadd1  27959  addsass  27975  negsproplem2  27998  negsproplem6  28002  negsid  28010  mulsval  28078  mulsrid  28082  mulsproplem2  28086  mulsproplem3  28087  mulsproplem4  28088  mulsproplem5  28089  mulsproplem6  28090  mulsproplem7  28091  mulsproplem8  28092  mulsproplem12  28096  mulscom  28108  addsdi  28124  precsexlem8  28182  precsexlem9  28183  precsexlem11  28185  eengbas  29003  ecgrtg  29005  reprsuc  34721  bnj1498  35166  mrsubcn  35662  mrsubco  35664  altxpsspw  36120  weiunse  36611  matunitlindflem1  37756  poimirlem9  37769  poimirlem22  37782  poimirlem31  37791  poimirlem32  37792  mbfresfi  37806  itg2addnclem2  37812  ftc1anclem7  37839  ftc1anc  37841  hdmaplem1  41970  hdmap1eulem  42021  sucidALTVD  45052  sucidALT  45053  founiiun0  45376  pimxrneun  45674  mccllem  45785  limcresiooub  45828  limcresioolb  45829  cnrefiisplem  46015  dvmptfprodlem  46130  dvnprodlem2  46133  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem54  46346  fourierdlem62  46354  fourierdlem71  46363  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  fouriersw  46417  nnfoctbdjlem  46641  hoidmvlelem2  46782  hoidmvlelem3  46783  pimrecltpos  46894  setsnidel  47565