Theorem elun2 4123

Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
elun2	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Proof of Theorem elun2

Step	Hyp	Ref	Expression
1		ssun2 4119	. 2 ⊢ 𝐵 ⊆ (𝐶 ∪ 𝐵)
2	1	sseli 3917	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  resf1extb  7885  dftpos4  8195  tfrlem11  8327  dif1en  9096  findcard2d  9101  cantnfp1lem1  9599  cantnfp1lem3  9601  tc2  9661  rankunb  9774  rankelun  9796  djurcl  9835  djuss  9844  djuun  9850  dfac2b  10053  cfsmolem  10192  isfin4p1  10237  zornn0g  10427  mnfxr  11202  supxrun  13268  fsumsplitsnun  15717  sumsplit  15730  modfsummodslem1  15755  prmreclem5  16891  acsfiindd  18519  lspsolv  21141  mplcoe1  22015  maducoeval2  22605  restntr  23147  1stckgenlem  23518  fbun  23805  filuni  23850  ufileu  23884  alexsubALTlem4  24015  tmdgsum  24060  icccmplem2  24789  aannenlem2  26295  aalioulem2  26299  noetainflem4  27704  eqcuts3  27796  cutlt  27924  addsval  27954  addsrid  27956  addscom  27958  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  leadds1  27981  addsass  27997  negsid  28033  mulsval  28101  mulsrid  28105  mulsproplem12  28119  mulscom  28131  addsdi  28147  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  oncutlt  28256  ebtwntg  29051  elntg  29053  elrspunsn  33489  bnj553  35040  bnj966  35086  bnj1442  35191  srcmpltd  35222  mrsubrn  35695  elmrsubrn  35702  mvhf  35740  msubvrs  35742  altxpsspw  36159  weiunse  36650  exrecfnlem  37695  matunitlindflem1  37937  poimirlem3  37944  poimirlem31  37972  poimirlem32  37973  mbfresfi  37987  itg2addnclem2  37993  ftc1anclem7  38020  ftc1anc  38022  hdmaplem2N  42218  hdmaplem3  42219  sucidVD  45298  nregmodellem  45443  pimxrneun  45916  mccllem  46027  limcresiooub  46070  limcresioolb  46071  cnrefiisplem  46257  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem1  46374  dvnprodlem2  46375  fourierdlem20  46555  fourierdlem38  46573  fourierdlem48  46582  fourierdlem49  46583  fourierdlem51  46585  fourierdlem62  46596  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem71  46605  fouriersw  46659  nnfoctbdjlem  46883  isomenndlem  46958  hoiprodp1  47016  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hspmbllem2  47055  pimrecltpos  47136  setsidel  47836