Theorem elun1 4134

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

Syntax hints:   → wi 4   ∈ wcel 2142   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is referenced by:  resf1extb  7915  brtpos  8215  dftpos4  8225  domunsncan  9049  unxpdomlem2  9201  rankunb  9808  rankelun  9830  djulcl  9868  djuss  9878  djuun  9884  fin1a2lem10  10366  zornn0g  10462  xrsupexmnf  13308  xrinfmexpnf  13309  sumsplit  15795  lcmfunsnlem2lem1  16672  lcmfunsnlem2  16674  prmreclem5  16956  smndex1mnd  18947  smndex1id  18948  gsumle  20185  lbsextlem3  21230  restntr  23242  comppfsc  23592  1stckgenlem  23613  fbun  23900  filconn  23943  filuni  23945  alexsubALTlem4  24110  ovolfiniun  25563  volfiniun  25609  elplyd  26262  ply1term  26264  aannenlem2  26393  aalioulem2  26397  eqcuts3  27897  cutlt  28025  addsval  28055  addsrid  28057  addscom  28059  addsproplem2  28063  addsproplem6  28067  leadds1  28082  addsass  28098  negsproplem2  28122  negsproplem6  28126  negsid  28134  mulsval  28202  mulsrid  28206  mulsproplem2  28210  mulsproplem3  28211  mulsproplem4  28212  mulsproplem5  28213  mulsproplem6  28214  mulsproplem7  28215  mulsproplem8  28216  mulsproplem12  28220  mulscom  28232  addsdi  28248  precsexlem8  28307  precsexlem9  28308  precsexlem11  28310  eengbas  29182  ecgrtg  29184  reprsuc  34909  bnj1498  35356  mrsubcn  35869  mrsubco  35871  altxpsspw  36327  weiunse  36828  matunitlindflem1  38115  poimirlem9  38128  poimirlem22  38141  poimirlem31  38150  poimirlem32  38151  mbfresfi  38165  itg2addnclem2  38171  ftc1anclem7  38198  ftc1anc  38200  hdmaplem1  42395  hdmap1eulem  42446  sucidALTVD  45445  sucidALT  45446  founiiun0  45768  pimxrneun  46062  mccllem  46173  limcresiooub  46216  limcresioolb  46217  cnrefiisplem  46403  dvmptfprodlem  46518  dvnprodlem2  46521  fourierdlem48  46728  fourierdlem49  46729  fourierdlem51  46731  fourierdlem54  46734  fourierdlem62  46742  fourierdlem71  46751  fourierdlem103  46783  fourierdlem104  46784  fourierdlem114  46794  fouriersw  46805  nnfoctbdjlem  47029  hoidmvlelem2  47170  hoidmvlelem3  47171  pimrecltpos  47282  setsnidel  47983