Theorem elun1 4157

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∪ cun 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943

This theorem is referenced by:  resf1extb  7930  brtpos  8234  dftpos4  8244  domunsncan  9086  unxpdomlem2  9259  rankunb  9864  rankelun  9886  djulcl  9924  djuss  9934  djuun  9940  fin1a2lem10  10423  zornn0g  10519  xrsupexmnf  13321  xrinfmexpnf  13322  sumsplit  15784  lcmfunsnlem2lem1  16657  lcmfunsnlem2  16659  prmreclem5  16940  smndex1mnd  18888  smndex1id  18889  lbsextlem3  21121  restntr  23120  comppfsc  23470  1stckgenlem  23491  fbun  23778  filconn  23821  filuni  23823  alexsubALTlem4  23988  ovolfiniun  25454  volfiniun  25500  elplyd  26159  ply1term  26161  aannenlem2  26289  aalioulem2  26293  cutlt  27892  addsval  27921  addsrid  27923  addscom  27925  addsproplem2  27929  addsproplem6  27933  sleadd1  27948  addsass  27964  negsproplem2  27987  negsproplem6  27991  negsid  27999  mulsval  28064  mulsrid  28068  mulsproplem2  28072  mulsproplem3  28073  mulsproplem4  28074  mulsproplem5  28075  mulsproplem6  28076  mulsproplem7  28077  mulsproplem8  28078  mulsproplem12  28082  mulscom  28094  addsdi  28110  precsexlem8  28168  precsexlem9  28169  precsexlem11  28171  eengbas  28960  ecgrtg  28962  gsumle  33092  reprsuc  34647  bnj1498  35092  mrsubcn  35541  mrsubco  35543  altxpsspw  35995  weiunse  36486  matunitlindflem1  37640  poimirlem9  37653  poimirlem22  37666  poimirlem31  37675  poimirlem32  37676  mbfresfi  37690  itg2addnclem2  37696  ftc1anclem7  37723  ftc1anc  37725  hdmaplem1  41790  hdmap1eulem  41841  metakunt21  42238  sucidALTVD  44894  sucidALT  44895  founiiun0  45214  pimxrneun  45515  mccllem  45626  limcresiooub  45671  limcresioolb  45672  cnrefiisplem  45858  dvmptfprodlem  45973  dvnprodlem2  45976  fourierdlem48  46183  fourierdlem49  46184  fourierdlem51  46186  fourierdlem54  46189  fourierdlem62  46197  fourierdlem71  46206  fourierdlem103  46238  fourierdlem104  46239  fourierdlem114  46249  fouriersw  46260  nnfoctbdjlem  46484  hoidmvlelem2  46625  hoidmvlelem3  46626  pimrecltpos  46737  setsnidel  47391