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  37655  poimirlem9  37668  poimirlem22  37681  poimirlem31  37690  poimirlem32  37691  mbfresfi  37705  itg2addnclem2  37711  ftc1anclem7  37738  ftc1anc  37740  hdmaplem1  41869  hdmap1eulem  41920  sucidALTVD  44961  sucidALT  44962  founiiun0  45286  pimxrneun  45585  mccllem  45696  limcresiooub  45739  limcresioolb  45740  cnrefiisplem  45926  dvmptfprodlem  46041  dvnprodlem2  46044  fourierdlem48  46251  fourierdlem49  46252  fourierdlem51  46254  fourierdlem54  46257  fourierdlem62  46265  fourierdlem71  46274  fourierdlem103  46306  fourierdlem104  46307  fourierdlem114  46317  fouriersw  46328  nnfoctbdjlem  46552  hoidmvlelem2  46693  hoidmvlelem3  46694  pimrecltpos  46805  setsnidel  47476