Theorem elun1 4177

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

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

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 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  brtpos  8220  dftpos4  8230  domunsncan  9072  unxpdomlem2  9251  rankunb  9845  rankelun  9867  djulcl  9905  djuss  9915  djuun  9921  fin1a2lem10  10404  zornn0g  10500  xrsupexmnf  13284  xrinfmexpnf  13285  sumsplit  15714  lcmfunsnlem2lem1  16575  lcmfunsnlem2  16577  prmreclem5  16853  smndex1mnd  18791  smndex1id  18792  lbsextlem3  20773  restntr  22686  comppfsc  23036  1stckgenlem  23057  fbun  23344  filconn  23387  filuni  23389  alexsubALTlem4  23554  ovolfiniun  25018  volfiniun  25064  elplyd  25716  ply1term  25718  aannenlem2  25842  aalioulem2  25846  cutlt  27419  addsval  27446  addsrid  27448  addscom  27450  addsproplem2  27454  addsproplem6  27458  sleadd1  27472  addsass  27488  negsproplem2  27503  negsproplem6  27507  negsid  27515  mulsval  27565  mulsrid  27569  mulsproplem2  27573  mulsproplem3  27574  mulsproplem4  27575  mulsproplem5  27576  mulsproplem6  27577  mulsproplem7  27578  mulsproplem8  27579  mulsproplem12  27583  mulscom  27595  addsdi  27610  precsexlem8  27660  precsexlem9  27661  precsexlem11  27663  eengbas  28239  ecgrtg  28241  gsumle  32242  reprsuc  33627  bnj1498  34072  mrsubcn  34510  mrsubco  34512  altxpsspw  34949  matunitlindflem1  36484  poimirlem9  36497  poimirlem22  36510  poimirlem31  36519  poimirlem32  36520  mbfresfi  36534  itg2addnclem2  36540  ftc1anclem7  36567  ftc1anc  36569  hdmaplem1  40642  hdmap1eulem  40693  metakunt21  41005  sucidALTVD  43631  sucidALT  43632  founiiun0  43888  pimxrneun  44199  mccllem  44313  limcresiooub  44358  limcresioolb  44359  cnrefiisplem  44545  dvmptfprodlem  44660  dvnprodlem2  44663  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem54  44876  fourierdlem62  44884  fourierdlem71  44893  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  fouriersw  44947  nnfoctbdjlem  45171  hoidmvlelem2  45312  hoidmvlelem3  45313  pimrecltpos  45424  setsnidel  46045