Theorem elun2 4112

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

Syntax hints:   → wi 4   ∈ wcel 2119   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  resf1extb  7874  dftpos4  8185  tfrlem11  8317  dif1en  9086  findcard2d  9091  cantnfp1lem1  9590  cantnfp1lem3  9592  tc2  9652  rankunb  9765  rankelun  9787  djurcl  9826  djuss  9835  djuun  9841  dfac2b  10044  cfsmolem  10183  isfin4p1  10228  zornn0g  10418  mnfxr  11193  supxrun  13259  fsumsplitsnun  15708  sumsplit  15721  modfsummodslem1  15746  prmreclem5  16882  acsfiindd  18510  lspsolv  21136  mplcoe1  22013  maducoeval2  22623  restntr  23165  1stckgenlem  23536  fbun  23823  filuni  23868  ufileu  23902  alexsubALTlem4  24033  tmdgsum  24078  icccmplem2  24807  aannenlem2  26313  aalioulem2  26317  noetainflem4  27722  eqcuts3  27814  cutlt  27942  addsval  27972  addsrid  27974  addscom  27976  addsproplem4  27982  addsproplem5  27983  addsproplem6  27984  leadds1  27999  addsass  28015  negsid  28051  mulsval  28119  mulsrid  28123  mulsproplem12  28137  mulscom  28149  addsdi  28165  precsexlem8  28224  precsexlem9  28225  precsexlem11  28227  oncutlt  28274  ebtwntg  29069  elntg  29071  elrspunsn  33512  mplidomlem  33711  bnj553  35080  bnj966  35126  bnj1442  35231  srcmpltd  35262  mrsubrn  35741  elmrsubrn  35748  mvhf  35786  msubvrs  35788  altxpsspw  36205  weiunse  36696  exrecfnlem  37741  matunitlindflem1  37983  poimirlem3  37990  poimirlem31  38018  poimirlem32  38019  mbfresfi  38033  itg2addnclem2  38039  ftc1anclem7  38066  ftc1anc  38068  hdmaplem2N  42264  hdmaplem3  42265  sucidVD  45315  nregmodellem  45460  pimxrneun  45931  mccllem  46042  limcresiooub  46085  limcresioolb  46086  cnrefiisplem  46272  dvmptfprodlem  46387  dvmptfprod  46388  dvnprodlem1  46389  dvnprodlem2  46390  fourierdlem20  46570  fourierdlem38  46588  fourierdlem48  46597  fourierdlem49  46598  fourierdlem51  46600  fourierdlem62  46611  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem71  46620  fouriersw  46674  nnfoctbdjlem  46898  isomenndlem  46973  hoiprodp1  47031  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hspmbllem2  47070  pimrecltpos  47151  setsidel  47851