Theorem elun1 4002

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∪ cun 3789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-un 3796  df-in 3798  df-ss 3805

This theorem is referenced by:  brtpos  7643  dftpos4  7653  domunsncan  8348  unxpdomlem2  8453  rankunb  9010  rankelun  9032  djulcl  9069  djuss  9079  djuun  9085  fin1a2lem10  9566  zornn0g  9662  xrsupexmnf  12447  xrinfmexpnf  12448  sumsplit  14904  lcmfunsnlem2lem1  15757  lcmfunsnlem2  15759  prmreclem5  16028  lbsextlem3  19557  restntr  21394  comppfsc  21744  1stckgenlem  21765  fbun  22052  filconn  22095  filuni  22097  alexsubALTlem4  22262  ovolfiniun  23705  volfiniun  23751  elplyd  24395  ply1term  24397  aannenlem2  24521  aalioulem2  24525  eengbas  26330  ecgrtg  26332  gsumle  30341  reprsuc  31295  bnj1498  31728  mrsubcn  32015  mrsubco  32017  altxpsspw  32673  matunitlindflem1  34015  poimirlem9  34028  poimirlem22  34041  poimirlem31  34050  poimirlem32  34051  mbfresfi  34065  itg2addnclem2  34071  ftc1anclem7  34100  ftc1anc  34102  hdmaplem1  37909  hdmap1eulem  37960  sucidALTVD  40021  sucidALT  40022  founiiun0  40282  mccllem  40719  limcresiooub  40764  limcresioolb  40765  cnrefiisplem  40951  dvmptfprodlem  41069  dvnprodlem2  41072  fourierdlem48  41280  fourierdlem49  41281  fourierdlem51  41283  fourierdlem54  41286  fourierdlem62  41294  fourierdlem71  41303  fourierdlem103  41335  fourierdlem104  41336  fourierdlem114  41346  fouriersw  41357  nnfoctbdjlem  41578  hoidmvlelem2  41719  hoidmvlelem3  41720  pimrecltpos  41828  setsnidel  42361