Theorem elun1 4145

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  resf1extb  7910  brtpos  8214  dftpos4  8224  domunsncan  9041  unxpdomlem2  9198  rankunb  9803  rankelun  9825  djulcl  9863  djuss  9873  djuun  9879  fin1a2lem10  10362  zornn0g  10458  xrsupexmnf  13265  xrinfmexpnf  13266  sumsplit  15734  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  prmreclem5  16891  smndex1mnd  18837  smndex1id  18838  lbsextlem3  21070  restntr  23069  comppfsc  23419  1stckgenlem  23440  fbun  23727  filconn  23770  filuni  23772  alexsubALTlem4  23937  ovolfiniun  25402  volfiniun  25448  elplyd  26107  ply1term  26109  aannenlem2  26237  aalioulem2  26241  cutlt  27840  addsval  27869  addsrid  27871  addscom  27873  addsproplem2  27877  addsproplem6  27881  sleadd1  27896  addsass  27912  negsproplem2  27935  negsproplem6  27939  negsid  27947  mulsval  28012  mulsrid  28016  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsproplem12  28030  mulscom  28042  addsdi  28058  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  eengbas  28908  ecgrtg  28910  gsumle  33038  reprsuc  34606  bnj1498  35051  mrsubcn  35506  mrsubco  35508  altxpsspw  35965  weiunse  36456  matunitlindflem1  37610  poimirlem9  37623  poimirlem22  37636  poimirlem31  37645  poimirlem32  37646  mbfresfi  37660  itg2addnclem2  37666  ftc1anclem7  37693  ftc1anc  37695  hdmaplem1  41765  hdmap1eulem  41816  sucidALTVD  44859  sucidALT  44860  founiiun0  45184  pimxrneun  45484  mccllem  45595  limcresiooub  45640  limcresioolb  45641  cnrefiisplem  45827  dvmptfprodlem  45942  dvnprodlem2  45945  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem62  46166  fourierdlem71  46175  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  fouriersw  46229  nnfoctbdjlem  46453  hoidmvlelem2  46594  hoidmvlelem3  46595  pimrecltpos  46706  setsnidel  47378