Theorem elun1 4136

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  resf1extb  7886  brtpos  8187  dftpos4  8197  domunsncan  9017  unxpdomlem2  9169  rankunb  9774  rankelun  9796  djulcl  9834  djuss  9844  djuun  9850  fin1a2lem10  10331  zornn0g  10427  xrsupexmnf  13232  xrinfmexpnf  13233  sumsplit  15703  lcmfunsnlem2lem1  16577  lcmfunsnlem2  16579  prmreclem5  16860  smndex1mnd  18847  smndex1id  18848  gsumle  20086  lbsextlem3  21127  restntr  23138  comppfsc  23488  1stckgenlem  23509  fbun  23796  filconn  23839  filuni  23841  alexsubALTlem4  24006  ovolfiniun  25470  volfiniun  25516  elplyd  26175  ply1term  26177  aannenlem2  26305  aalioulem2  26309  eqcuts3  27812  cutlt  27940  addsval  27970  addsrid  27972  addscom  27974  addsproplem2  27978  addsproplem6  27982  leadds1  27997  addsass  28013  negsproplem2  28037  negsproplem6  28041  negsid  28049  mulsval  28117  mulsrid  28121  mulsproplem2  28125  mulsproplem3  28126  mulsproplem4  28127  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  mulsproplem12  28135  mulscom  28147  addsdi  28163  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  eengbas  29066  ecgrtg  29068  reprsuc  34793  bnj1498  35237  mrsubcn  35735  mrsubco  35737  altxpsspw  36193  weiunse  36684  matunitlindflem1  37867  poimirlem9  37880  poimirlem22  37893  poimirlem31  37902  poimirlem32  37903  mbfresfi  37917  itg2addnclem2  37923  ftc1anclem7  37950  ftc1anc  37952  hdmaplem1  42147  hdmap1eulem  42198  sucidALTVD  45225  sucidALT  45226  founiiun0  45549  pimxrneun  45846  mccllem  45957  limcresiooub  46000  limcresioolb  46001  cnrefiisplem  46187  dvmptfprodlem  46302  dvnprodlem2  46305  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem54  46518  fourierdlem62  46526  fourierdlem71  46535  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  fouriersw  46589  nnfoctbdjlem  46813  hoidmvlelem2  46954  hoidmvlelem3  46955  pimrecltpos  47066  setsnidel  47737