Theorem elun1 4182

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∪ cun 4151

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-un 4153

This theorem is used by:  resf1extb  7953  brtpos  8263  dftpos4  8273  domunsncan  9107  unxpdomlem2  9259  rankunb  9874  rankelun  9899  djulcl  10001  djuss  10011  djuun  10017  fin1a2lem10  10497  zornn0g  10593  xrsupexmnf  13445  xrinfmexpnf  13446  sumsplit  15946  lcmfunsnlem2lem1  16825  lcmfunsnlem2  16827  prmreclem5  17110  smndex1mnd  19121  smndex1id  19122  gsumle  20371  lbsextlem3  21450  matunitlindflem1  23006  restntr  23512  comppfsc  23863  1stckgenlem  23884  fbun  24171  filconn  24214  filuni  24216  alexsubALTlem4  24381  ovolfiniun  25834  volfiniun  25880  elplyd  26532  ply1term  26534  aannenlem2  26668  aalioulem2  26672  eqcuts3  28202  cutlt  28330  addsval  28360  addsrid  28362  addscom  28364  addsproplem2  28368  addsproplem6  28372  leadds1  28387  addsass  28403  negsproplem2  28427  negsproplem6  28431  negsid  28439  mulsval  28507  mulsrid  28511  mulsproplem2  28515  mulsproplem3  28516  mulsproplem4  28517  mulsproplem5  28518  mulsproplem6  28519  mulsproplem7  28520  mulsproplem8  28521  mulsproplem12  28525  mulscom  28537  addsdi  28553  precsexlem8  28612  precsexlem9  28613  precsexlem11  28615  eengbas  29571  ecgrtg  29573  reprsuc  35297  bnj1498  35744  mrsubcn  36405  mrsubco  36407  altxpsspw  36869  weiunse  37383  poimirlem9  38687  poimirlem22  38700  poimirlem31  38709  poimirlem32  38710  mbfresfi  38724  itg2addnclem2  38730  ftc1anclem7  38757  ftc1anc  38759  hdmaplem1  42968  hdmap1eulem  43019  sucidALTVD  45991  sucidALT  45992  founiiun0  46344  pimxrneun  46637  mccllem  46748  limcresiooub  46791  limcresioolb  46792  cnrefiisplem  46978  dvmptfprodlem  47093  dvnprodlem2  47096  fourierdlem48  47303  fourierdlem49  47304  fourierdlem51  47306  fourierdlem54  47309  fourierdlem62  47317  fourierdlem71  47326  fourierdlem103  47358  fourierdlem104  47359  fourierdlem114  47369  fouriersw  47380  nnfoctbdjlem  47604  hoidmvlelem2  47745  hoidmvlelem3  47746  pimrecltpos  47857  setsnidel  48598