Theorem elun1 4133

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

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

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 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  resf1extb  7867  brtpos  8168  dftpos4  8178  domunsncan  8994  unxpdomlem2  9146  rankunb  9746  rankelun  9768  djulcl  9806  djuss  9816  djuun  9822  fin1a2lem10  10303  zornn0g  10399  xrsupexmnf  13207  xrinfmexpnf  13208  sumsplit  15675  lcmfunsnlem2lem1  16549  lcmfunsnlem2  16551  prmreclem5  16832  smndex1mnd  18784  smndex1id  18785  gsumle  20024  lbsextlem3  21067  restntr  23067  comppfsc  23417  1stckgenlem  23438  fbun  23725  filconn  23768  filuni  23770  alexsubALTlem4  23935  ovolfiniun  25400  volfiniun  25446  elplyd  26105  ply1term  26107  aannenlem2  26235  aalioulem2  26239  eqscut3  27735  cutlt  27845  addsval  27874  addsrid  27876  addscom  27878  addsproplem2  27882  addsproplem6  27886  sleadd1  27901  addsass  27917  negsproplem2  27940  negsproplem6  27944  negsid  27952  mulsval  28017  mulsrid  28021  mulsproplem2  28025  mulsproplem3  28026  mulsproplem4  28027  mulsproplem5  28028  mulsproplem6  28029  mulsproplem7  28030  mulsproplem8  28031  mulsproplem12  28035  mulscom  28047  addsdi  28063  precsexlem8  28121  precsexlem9  28122  precsexlem11  28124  eengbas  28926  ecgrtg  28928  reprsuc  34583  bnj1498  35028  mrsubcn  35496  mrsubco  35498  altxpsspw  35955  weiunse  36446  matunitlindflem1  37600  poimirlem9  37613  poimirlem22  37626  poimirlem31  37635  poimirlem32  37636  mbfresfi  37650  itg2addnclem2  37656  ftc1anclem7  37683  ftc1anc  37685  hdmaplem1  41754  hdmap1eulem  41805  sucidALTVD  44847  sucidALT  44848  founiiun0  45172  pimxrneun  45471  mccllem  45582  limcresiooub  45627  limcresioolb  45628  cnrefiisplem  45814  dvmptfprodlem  45929  dvnprodlem2  45932  fourierdlem48  46139  fourierdlem49  46140  fourierdlem51  46142  fourierdlem54  46145  fourierdlem62  46153  fourierdlem71  46162  fourierdlem103  46194  fourierdlem104  46195  fourierdlem114  46205  fouriersw  46216  nnfoctbdjlem  46440  hoidmvlelem2  46581  hoidmvlelem3  46582  pimrecltpos  46693  setsnidel  47365