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 3929	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2113   ∪ cun 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  resf1extb  7876  brtpos  8177  dftpos4  8187  domunsncan  9005  unxpdomlem2  9157  rankunb  9762  rankelun  9784  djulcl  9822  djuss  9832  djuun  9838  fin1a2lem10  10319  zornn0g  10415  xrsupexmnf  13220  xrinfmexpnf  13221  sumsplit  15691  lcmfunsnlem2lem1  16565  lcmfunsnlem2  16567  prmreclem5  16848  smndex1mnd  18835  smndex1id  18836  gsumle  20074  lbsextlem3  21115  restntr  23126  comppfsc  23476  1stckgenlem  23497  fbun  23784  filconn  23827  filuni  23829  alexsubALTlem4  23994  ovolfiniun  25458  volfiniun  25504  elplyd  26163  ply1term  26165  aannenlem2  26293  aalioulem2  26297  eqcuts3  27800  cutlt  27928  addsval  27958  addsrid  27960  addscom  27962  addsproplem2  27966  addsproplem6  27970  leadds1  27985  addsass  28001  negsproplem2  28025  negsproplem6  28029  negsid  28037  mulsval  28105  mulsrid  28109  mulsproplem2  28113  mulsproplem3  28114  mulsproplem4  28115  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  mulsproplem12  28123  mulscom  28135  addsdi  28151  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  eengbas  29054  ecgrtg  29056  reprsuc  34772  bnj1498  35217  mrsubcn  35713  mrsubco  35715  altxpsspw  36171  weiunse  36662  matunitlindflem1  37817  poimirlem9  37830  poimirlem22  37843  poimirlem31  37852  poimirlem32  37853  mbfresfi  37867  itg2addnclem2  37873  ftc1anclem7  37900  ftc1anc  37902  hdmaplem1  42041  hdmap1eulem  42092  sucidALTVD  45120  sucidALT  45121  founiiun0  45444  pimxrneun  45742  mccllem  45853  limcresiooub  45896  limcresioolb  45897  cnrefiisplem  46083  dvmptfprodlem  46198  dvnprodlem2  46201  fourierdlem48  46408  fourierdlem49  46409  fourierdlem51  46411  fourierdlem54  46414  fourierdlem62  46422  fourierdlem71  46431  fourierdlem103  46463  fourierdlem104  46464  fourierdlem114  46474  fouriersw  46485  nnfoctbdjlem  46709  hoidmvlelem2  46850  hoidmvlelem3  46851  pimrecltpos  46962  setsnidel  47633