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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  resf1extb  7946  brtpos  8252  dftpos4  8262  domunsncan  9096  unxpdomlem2  9248  rankunb  9864  rankelun  9889  djulcl  9991  djuss  10001  djuun  10007  fin1a2lem10  10487  zornn0g  10583  xrsupexmnf  13435  xrinfmexpnf  13436  sumsplit  15934  lcmfunsnlem2lem1  16813  lcmfunsnlem2  16815  prmreclem5  17098  smndex1mnd  19109  smndex1id  19110  gsumle  20359  lbsextlem3  21438  matunitlindflem1  22994  restntr  23500  comppfsc  23851  1stckgenlem  23872  fbun  24159  filconn  24202  filuni  24204  alexsubALTlem4  24369  ovolfiniun  25822  volfiniun  25868  elplyd  26520  ply1term  26522  aannenlem2  26656  aalioulem2  26660  eqcuts3  28190  cutlt  28318  addsval  28348  addsrid  28350  addscom  28352  addsproplem2  28356  addsproplem6  28360  leadds1  28375  addsass  28391  negsproplem2  28415  negsproplem6  28419  negsid  28427  mulsval  28495  mulsrid  28499  mulsproplem2  28503  mulsproplem3  28504  mulsproplem4  28505  mulsproplem5  28506  mulsproplem6  28507  mulsproplem7  28508  mulsproplem8  28509  mulsproplem12  28513  mulscom  28525  addsdi  28541  precsexlem8  28600  precsexlem9  28601  precsexlem11  28603  eengbas  29559  ecgrtg  29561  reprsuc  35244  bnj1498  35691  mrsubcn  36284  mrsubco  36286  altxpsspw  36742  weiunse  37256  poimirlem9  38547  poimirlem22  38560  poimirlem31  38569  poimirlem32  38570  mbfresfi  38584  itg2addnclem2  38590  ftc1anclem7  38617  ftc1anc  38619  hdmaplem1  42828  hdmap1eulem  42879  sucidALTVD  45851  sucidALT  45852  founiiun0  46204  pimxrneun  46497  mccllem  46608  limcresiooub  46651  limcresioolb  46652  cnrefiisplem  46838  dvmptfprodlem  46953  dvnprodlem2  46956  fourierdlem48  47163  fourierdlem49  47164  fourierdlem51  47166  fourierdlem54  47169  fourierdlem62  47177  fourierdlem71  47186  fourierdlem103  47218  fourierdlem104  47219  fourierdlem114  47229  fouriersw  47240  nnfoctbdjlem  47464  hoidmvlelem2  47605  hoidmvlelem3  47606  pimrecltpos  47717  setsnidel  48458