Theorem elun1 4122

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  resf1extb  7885  brtpos  8185  dftpos4  8195  domunsncan  9015  unxpdomlem2  9167  rankunb  9774  rankelun  9796  djulcl  9834  djuss  9844  djuun  9850  fin1a2lem10  10331  zornn0g  10427  xrsupexmnf  13257  xrinfmexpnf  13258  sumsplit  15730  lcmfunsnlem2lem1  16607  lcmfunsnlem2  16609  prmreclem5  16891  smndex1mnd  18881  smndex1id  18882  gsumle  20120  lbsextlem3  21158  restntr  23147  comppfsc  23497  1stckgenlem  23518  fbun  23805  filconn  23848  filuni  23850  alexsubALTlem4  24015  ovolfiniun  25468  volfiniun  25514  elplyd  26167  ply1term  26169  aannenlem2  26295  aalioulem2  26299  eqcuts3  27796  cutlt  27924  addsval  27954  addsrid  27956  addscom  27958  addsproplem2  27962  addsproplem6  27966  leadds1  27981  addsass  27997  negsproplem2  28021  negsproplem6  28025  negsid  28033  mulsval  28101  mulsrid  28105  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsproplem12  28119  mulscom  28131  addsdi  28147  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  eengbas  29050  ecgrtg  29052  reprsuc  34759  bnj1498  35203  mrsubcn  35701  mrsubco  35703  altxpsspw  36159  weiunse  36650  matunitlindflem1  37937  poimirlem9  37950  poimirlem22  37963  poimirlem31  37972  poimirlem32  37973  mbfresfi  37987  itg2addnclem2  37993  ftc1anclem7  38020  ftc1anc  38022  hdmaplem1  42217  hdmap1eulem  42268  sucidALTVD  45296  sucidALT  45297  founiiun0  45620  pimxrneun  45916  mccllem  46027  limcresiooub  46070  limcresioolb  46071  cnrefiisplem  46257  dvmptfprodlem  46372  dvnprodlem2  46375  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem62  46596  fourierdlem71  46605  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  fouriersw  46659  nnfoctbdjlem  46883  hoidmvlelem2  47024  hoidmvlelem3  47025  pimrecltpos  47136  setsnidel  47837