Theorem elun1 4192

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  brtpos  8259  dftpos4  8269  domunsncan  9111  unxpdomlem2  9285  rankunb  9888  rankelun  9910  djulcl  9948  djuss  9958  djuun  9964  fin1a2lem10  10447  zornn0g  10543  xrsupexmnf  13344  xrinfmexpnf  13345  sumsplit  15801  lcmfunsnlem2lem1  16672  lcmfunsnlem2  16674  prmreclem5  16954  smndex1mnd  18936  smndex1id  18937  lbsextlem3  21180  restntr  23206  comppfsc  23556  1stckgenlem  23577  fbun  23864  filconn  23907  filuni  23909  alexsubALTlem4  24074  ovolfiniun  25550  volfiniun  25596  elplyd  26256  ply1term  26258  aannenlem2  26386  aalioulem2  26390  cutlt  27981  addsval  28010  addsrid  28012  addscom  28014  addsproplem2  28018  addsproplem6  28022  sleadd1  28037  addsass  28053  negsproplem2  28076  negsproplem6  28080  negsid  28088  mulsval  28150  mulsrid  28154  mulsproplem2  28158  mulsproplem3  28159  mulsproplem4  28160  mulsproplem5  28161  mulsproplem6  28162  mulsproplem7  28163  mulsproplem8  28164  mulsproplem12  28168  mulscom  28180  addsdi  28196  precsexlem8  28253  precsexlem9  28254  precsexlem11  28256  eengbas  29011  ecgrtg  29013  gsumle  33084  reprsuc  34609  bnj1498  35054  mrsubcn  35504  mrsubco  35506  altxpsspw  35959  weiunse  36451  matunitlindflem1  37603  poimirlem9  37616  poimirlem22  37629  poimirlem31  37638  poimirlem32  37639  mbfresfi  37653  itg2addnclem2  37659  ftc1anclem7  37686  ftc1anc  37688  hdmaplem1  41754  hdmap1eulem  41805  metakunt21  42207  sucidALTVD  44868  sucidALT  44869  founiiun0  45133  pimxrneun  45439  mccllem  45553  limcresiooub  45598  limcresioolb  45599  cnrefiisplem  45785  dvmptfprodlem  45900  dvnprodlem2  45903  fourierdlem48  46110  fourierdlem49  46111  fourierdlem51  46113  fourierdlem54  46116  fourierdlem62  46124  fourierdlem71  46133  fourierdlem103  46165  fourierdlem104  46166  fourierdlem114  46176  fouriersw  46187  nnfoctbdjlem  46411  hoidmvlelem2  46552  hoidmvlelem3  46553  pimrecltpos  46664  setsnidel  47302