Theorem elun1 4128

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  resf1extb  7932  brtpos  8234  dftpos4  8244  domunsncan  9076  unxpdomlem2  9228  rankunb  9833  rankelun  9855  djulcl  9916  djuss  9926  djuun  9932  fin1a2lem10  10412  zornn0g  10508  xrsupexmnf  13358  xrinfmexpnf  13359  sumsplit  15855  lcmfunsnlem2lem1  16729  lcmfunsnlem2  16731  prmreclem5  17013  smndex1mnd  19023  smndex1id  19024  gsumle  20273  lbsextlem3  21348  matunitlindflem1  22902  restntr  23408  comppfsc  23759  1stckgenlem  23780  fbun  24067  filconn  24110  filuni  24112  alexsubALTlem4  24277  ovolfiniun  25730  volfiniun  25776  elplyd  26428  ply1term  26430  aannenlem2  26566  aalioulem2  26570  eqcuts3  28070  cutlt  28198  addsval  28228  addsrid  28230  addscom  28232  addsproplem2  28236  addsproplem6  28240  leadds1  28255  addsass  28271  negsproplem2  28295  negsproplem6  28299  negsid  28307  mulsval  28375  mulsrid  28379  mulsproplem2  28383  mulsproplem3  28384  mulsproplem4  28385  mulsproplem5  28386  mulsproplem6  28387  mulsproplem7  28388  mulsproplem8  28389  mulsproplem12  28393  mulscom  28405  addsdi  28421  precsexlem8  28480  precsexlem9  28481  precsexlem11  28483  eengbas  29439  ecgrtg  29441  reprsuc  35124  bnj1498  35571  mrsubcn  36099  mrsubco  36101  altxpsspw  36558  weiunse  37088  poimirlem9  38379  poimirlem22  38392  poimirlem31  38401  poimirlem32  38402  mbfresfi  38416  itg2addnclem2  38422  ftc1anclem7  38449  ftc1anc  38451  hdmaplem1  42645  hdmap1eulem  42696  sucidALTVD  45693  sucidALT  45694  founiiun0  46023  pimxrneun  46317  mccllem  46428  limcresiooub  46471  limcresioolb  46472  cnrefiisplem  46658  dvmptfprodlem  46773  dvnprodlem2  46776  fourierdlem48  46983  fourierdlem49  46984  fourierdlem51  46986  fourierdlem54  46989  fourierdlem62  46997  fourierdlem71  47006  fourierdlem103  47038  fourierdlem104  47039  fourierdlem114  47049  fouriersw  47060  nnfoctbdjlem  47284  hoidmvlelem2  47425  hoidmvlelem3  47426  pimrecltpos  47537  setsnidel  48278