Theorem elun1 4143

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  resf1extb  7931  brtpos  8231  dftpos4  8241  domunsncan  9065  unxpdomlem2  9217  rankunb  9822  rankelun  9844  djulcl  9896  djuss  9906  djuun  9912  fin1a2lem10  10393  zornn0g  10489  xrsupexmnf  13331  xrinfmexpnf  13332  sumsplit  15819  lcmfunsnlem2lem1  16696  lcmfunsnlem2  16698  prmreclem5  16980  smndex1mnd  18972  smndex1id  18973  gsumle  20215  lbsextlem3  21262  restntr  23308  comppfsc  23658  1stckgenlem  23679  fbun  23966  filconn  24009  filuni  24011  alexsubALTlem4  24176  ovolfiniun  25629  volfiniun  25675  elplyd  26328  ply1term  26330  aannenlem2  26459  aalioulem2  26463  eqcuts3  27963  cutlt  28091  addsval  28121  addsrid  28123  addscom  28125  addsproplem2  28129  addsproplem6  28133  leadds1  28148  addsass  28164  negsproplem2  28188  negsproplem6  28192  negsid  28200  mulsval  28268  mulsrid  28272  mulsproplem2  28276  mulsproplem3  28277  mulsproplem4  28278  mulsproplem5  28279  mulsproplem6  28280  mulsproplem7  28281  mulsproplem8  28282  mulsproplem12  28286  mulscom  28298  addsdi  28314  precsexlem8  28373  precsexlem9  28374  precsexlem11  28376  eengbas  29272  ecgrtg  29274  reprsuc  34947  bnj1498  35394  mrsubcn  35910  mrsubco  35912  altxpsspw  36368  weiunse  36868  matunitlindflem1  38155  poimirlem9  38168  poimirlem22  38181  poimirlem31  38190  poimirlem32  38191  mbfresfi  38205  itg2addnclem2  38211  ftc1anclem7  38238  ftc1anc  38240  hdmaplem1  42435  hdmap1eulem  42486  sucidALTVD  45470  sucidALT  45471  founiiun0  45800  pimxrneun  46094  mccllem  46205  limcresiooub  46248  limcresioolb  46249  cnrefiisplem  46435  dvmptfprodlem  46550  dvnprodlem2  46553  fourierdlem48  46760  fourierdlem49  46761  fourierdlem51  46763  fourierdlem54  46766  fourierdlem62  46774  fourierdlem71  46783  fourierdlem103  46815  fourierdlem104  46816  fourierdlem114  46826  fouriersw  46837  nnfoctbdjlem  47061  hoidmvlelem2  47202  hoidmvlelem3  47203  pimrecltpos  47314  setsnidel  48015