Theorem elun1 4129

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∪ cun 3895

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  resf1extb  7864  brtpos  8165  dftpos4  8175  domunsncan  8990  unxpdomlem2  9141  rankunb  9743  rankelun  9765  djulcl  9803  djuss  9813  djuun  9819  fin1a2lem10  10300  zornn0g  10396  xrsupexmnf  13204  xrinfmexpnf  13205  sumsplit  15675  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  prmreclem5  16832  smndex1mnd  18818  smndex1id  18819  gsumle  20057  lbsextlem3  21097  restntr  23097  comppfsc  23447  1stckgenlem  23468  fbun  23755  filconn  23798  filuni  23800  alexsubALTlem4  23965  ovolfiniun  25429  volfiniun  25475  elplyd  26134  ply1term  26136  aannenlem2  26264  aalioulem2  26268  eqscut3  27765  cutlt  27876  addsval  27905  addsrid  27907  addscom  27909  addsproplem2  27913  addsproplem6  27917  sleadd1  27932  addsass  27948  negsproplem2  27971  negsproplem6  27975  negsid  27983  mulsval  28048  mulsrid  28052  mulsproplem2  28056  mulsproplem3  28057  mulsproplem4  28058  mulsproplem5  28059  mulsproplem6  28060  mulsproplem7  28061  mulsproplem8  28062  mulsproplem12  28066  mulscom  28078  addsdi  28094  precsexlem8  28152  precsexlem9  28153  precsexlem11  28155  eengbas  28959  ecgrtg  28961  reprsuc  34628  bnj1498  35073  mrsubcn  35563  mrsubco  35565  altxpsspw  36021  weiunse  36512  matunitlindflem1  37666  poimirlem9  37679  poimirlem22  37692  poimirlem31  37701  poimirlem32  37702  mbfresfi  37716  itg2addnclem2  37722  ftc1anclem7  37749  ftc1anc  37751  hdmaplem1  41880  hdmap1eulem  41931  sucidALTVD  44972  sucidALT  44973  founiiun0  45297  pimxrneun  45596  mccllem  45707  limcresiooub  45750  limcresioolb  45751  cnrefiisplem  45937  dvmptfprodlem  46052  dvnprodlem2  46055  fourierdlem48  46262  fourierdlem49  46263  fourierdlem51  46265  fourierdlem54  46268  fourierdlem62  46276  fourierdlem71  46285  fourierdlem103  46317  fourierdlem104  46318  fourierdlem114  46328  fouriersw  46339  nnfoctbdjlem  46563  hoidmvlelem2  46704  hoidmvlelem3  46705  pimrecltpos  46816  setsnidel  47487