Theorem elun1 4111

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  resf1extb  7874  brtpos  8175  dftpos4  8185  domunsncan  9005  unxpdomlem2  9157  rankunb  9765  rankelun  9787  djulcl  9825  djuss  9835  djuun  9841  fin1a2lem10  10322  zornn0g  10418  xrsupexmnf  13248  xrinfmexpnf  13249  sumsplit  15721  lcmfunsnlem2lem1  16598  lcmfunsnlem2  16600  prmreclem5  16882  smndex1mnd  18872  smndex1id  18873  gsumle  20111  lbsextlem3  21153  restntr  23165  comppfsc  23515  1stckgenlem  23536  fbun  23823  filconn  23866  filuni  23868  alexsubALTlem4  24033  ovolfiniun  25486  volfiniun  25532  elplyd  26185  ply1term  26187  aannenlem2  26313  aalioulem2  26317  eqcuts3  27814  cutlt  27942  addsval  27972  addsrid  27974  addscom  27976  addsproplem2  27980  addsproplem6  27984  leadds1  27999  addsass  28015  negsproplem2  28039  negsproplem6  28043  negsid  28051  mulsval  28119  mulsrid  28123  mulsproplem2  28127  mulsproplem3  28128  mulsproplem4  28129  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  mulsproplem12  28137  mulscom  28149  addsdi  28165  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  eengbas  29068  ecgrtg  29070  reprsuc  34799  bnj1498  35243  mrsubcn  35747  mrsubco  35749  altxpsspw  36205  weiunse  36696  matunitlindflem1  37983  poimirlem9  37996  poimirlem22  38009  poimirlem31  38018  poimirlem32  38019  mbfresfi  38033  itg2addnclem2  38039  ftc1anclem7  38066  ftc1anc  38068  hdmaplem1  42263  hdmap1eulem  42314  sucidALTVD  45313  sucidALT  45314  founiiun0  45637  pimxrneun  45931  mccllem  46042  limcresiooub  46085  limcresioolb  46086  cnrefiisplem  46272  dvmptfprodlem  46387  dvnprodlem2  46390  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem54  46603  fourierdlem62  46611  fourierdlem71  46620  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  fouriersw  46674  nnfoctbdjlem  46898  hoidmvlelem2  47039  hoidmvlelem3  47040  pimrecltpos  47151  setsnidel  47852