Theorem elun1 4174

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∪ cun 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3951  df-in 3953  df-ss 3963

This theorem is referenced by:  brtpos  8214  dftpos4  8224  domunsncan  9067  unxpdomlem2  9246  rankunb  9840  rankelun  9862  djulcl  9900  djuss  9910  djuun  9916  fin1a2lem10  10399  zornn0g  10495  xrsupexmnf  13279  xrinfmexpnf  13280  sumsplit  15709  lcmfunsnlem2lem1  16570  lcmfunsnlem2  16572  prmreclem5  16848  smndex1mnd  18786  smndex1id  18787  lbsextlem3  20760  restntr  22667  comppfsc  23017  1stckgenlem  23038  fbun  23325  filconn  23368  filuni  23370  alexsubALTlem4  23535  ovolfiniun  24999  volfiniun  25045  elplyd  25697  ply1term  25699  aannenlem2  25823  aalioulem2  25827  cutlt  27398  addsval  27425  addsrid  27427  addscom  27429  addsproplem2  27433  addsproplem6  27437  sleadd1  27451  addsass  27467  negsproplem2  27482  negsproplem6  27486  negsid  27494  mulsval  27544  mulsrid  27548  mulsproplem2  27552  mulsproplem3  27553  mulsproplem4  27554  mulsproplem5  27555  mulsproplem6  27556  mulsproplem7  27557  mulsproplem8  27558  mulsproplem12  27562  mulscom  27574  addsdi  27589  precsexlem8  27639  precsexlem9  27640  precsexlem11  27642  eengbas  28218  ecgrtg  28220  gsumle  32219  reprsuc  33564  bnj1498  34009  mrsubcn  34447  mrsubco  34449  altxpsspw  34886  matunitlindflem1  36421  poimirlem9  36434  poimirlem22  36447  poimirlem31  36456  poimirlem32  36457  mbfresfi  36471  itg2addnclem2  36477  ftc1anclem7  36504  ftc1anc  36506  hdmaplem1  40579  hdmap1eulem  40630  metakunt21  40942  sucidALTVD  43563  sucidALT  43564  founiiun0  43820  pimxrneun  44133  mccllem  44247  limcresiooub  44292  limcresioolb  44293  cnrefiisplem  44479  dvmptfprodlem  44594  dvnprodlem2  44597  fourierdlem48  44804  fourierdlem49  44805  fourierdlem51  44807  fourierdlem54  44810  fourierdlem62  44818  fourierdlem71  44827  fourierdlem103  44859  fourierdlem104  44860  fourierdlem114  44870  fouriersw  44881  nnfoctbdjlem  45105  hoidmvlelem2  45246  hoidmvlelem3  45247  pimrecltpos  45358  setsnidel  45979