Theorem elun1 4182

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  resf1extb  7956  brtpos  8260  dftpos4  8270  domunsncan  9112  unxpdomlem2  9287  rankunb  9890  rankelun  9912  djulcl  9950  djuss  9960  djuun  9966  fin1a2lem10  10449  zornn0g  10545  xrsupexmnf  13347  xrinfmexpnf  13348  sumsplit  15804  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  prmreclem5  16958  smndex1mnd  18923  smndex1id  18924  lbsextlem3  21162  restntr  23190  comppfsc  23540  1stckgenlem  23561  fbun  23848  filconn  23891  filuni  23893  alexsubALTlem4  24058  ovolfiniun  25536  volfiniun  25582  elplyd  26241  ply1term  26243  aannenlem2  26371  aalioulem2  26375  cutlt  27966  addsval  27995  addsrid  27997  addscom  27999  addsproplem2  28003  addsproplem6  28007  sleadd1  28022  addsass  28038  negsproplem2  28061  negsproplem6  28065  negsid  28073  mulsval  28135  mulsrid  28139  mulsproplem2  28143  mulsproplem3  28144  mulsproplem4  28145  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  mulsproplem12  28153  mulscom  28165  addsdi  28181  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  eengbas  28996  ecgrtg  28998  gsumle  33101  reprsuc  34630  bnj1498  35075  mrsubcn  35524  mrsubco  35526  altxpsspw  35978  weiunse  36469  matunitlindflem1  37623  poimirlem9  37636  poimirlem22  37649  poimirlem31  37658  poimirlem32  37659  mbfresfi  37673  itg2addnclem2  37679  ftc1anclem7  37706  ftc1anc  37708  hdmaplem1  41773  hdmap1eulem  41824  metakunt21  42226  sucidALTVD  44890  sucidALT  44891  founiiun0  45195  pimxrneun  45499  mccllem  45612  limcresiooub  45657  limcresioolb  45658  cnrefiisplem  45844  dvmptfprodlem  45959  dvnprodlem2  45962  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem62  46183  fourierdlem71  46192  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  fouriersw  46246  nnfoctbdjlem  46470  hoidmvlelem2  46611  hoidmvlelem3  46612  pimrecltpos  46723  setsnidel  47364