Theorem elun1 4176

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  brtpos  8217  dftpos4  8227  domunsncan  9069  unxpdomlem2  9248  rankunb  9842  rankelun  9864  djulcl  9902  djuss  9912  djuun  9918  fin1a2lem10  10401  zornn0g  10497  xrsupexmnf  13281  xrinfmexpnf  13282  sumsplit  15711  lcmfunsnlem2lem1  16572  lcmfunsnlem2  16574  prmreclem5  16850  smndex1mnd  18788  smndex1id  18789  lbsextlem3  20766  restntr  22678  comppfsc  23028  1stckgenlem  23049  fbun  23336  filconn  23379  filuni  23381  alexsubALTlem4  23546  ovolfiniun  25010  volfiniun  25056  elplyd  25708  ply1term  25710  aannenlem2  25834  aalioulem2  25838  cutlt  27409  addsval  27436  addsrid  27438  addscom  27440  addsproplem2  27444  addsproplem6  27448  sleadd1  27462  addsass  27478  negsproplem2  27493  negsproplem6  27497  negsid  27505  mulsval  27555  mulsrid  27559  mulsproplem2  27563  mulsproplem3  27564  mulsproplem4  27565  mulsproplem5  27566  mulsproplem6  27567  mulsproplem7  27568  mulsproplem8  27569  mulsproplem12  27573  mulscom  27585  addsdi  27600  precsexlem8  27650  precsexlem9  27651  precsexlem11  27653  eengbas  28229  ecgrtg  28231  gsumle  32230  reprsuc  33616  bnj1498  34061  mrsubcn  34499  mrsubco  34501  altxpsspw  34938  matunitlindflem1  36473  poimirlem9  36486  poimirlem22  36499  poimirlem31  36508  poimirlem32  36509  mbfresfi  36523  itg2addnclem2  36529  ftc1anclem7  36556  ftc1anc  36558  hdmaplem1  40631  hdmap1eulem  40682  metakunt21  40994  sucidALTVD  43617  sucidALT  43618  founiiun0  43874  pimxrneun  44186  mccllem  44300  limcresiooub  44345  limcresioolb  44346  cnrefiisplem  44532  dvmptfprodlem  44647  dvnprodlem2  44650  fourierdlem48  44857  fourierdlem49  44858  fourierdlem51  44860  fourierdlem54  44863  fourierdlem62  44871  fourierdlem71  44880  fourierdlem103  44912  fourierdlem104  44913  fourierdlem114  44923  fouriersw  44934  nnfoctbdjlem  45158  hoidmvlelem2  45299  hoidmvlelem3  45300  pimrecltpos  45411  setsnidel  46032