Theorem elun2 4134

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∪ cun 3901

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  resf1extb  7867  dftpos4  8178  tfrlem11  8310  dif1en  9075  findcard2d  9080  cantnfp1lem1  9574  cantnfp1lem3  9576  tc2  9638  rankunb  9746  rankelun  9768  djurcl  9807  djuss  9816  djuun  9822  dfac2b  10025  cfsmolem  10164  isfin4p1  10209  zornn0g  10399  mnfxr  11172  supxrun  13218  fsumsplitsnun  15662  sumsplit  15675  modfsummodslem1  15699  prmreclem5  16832  acsfiindd  18459  lspsolv  21050  mplcoe1  21942  maducoeval2  22525  restntr  23067  1stckgenlem  23438  fbun  23725  filuni  23770  ufileu  23804  alexsubALTlem4  23935  tmdgsum  23980  icccmplem2  24710  aannenlem2  26235  aalioulem2  26239  noetainflem4  27650  eqscut3  27736  cutlt  27847  addsval  27876  addsrid  27878  addscom  27880  addsproplem4  27886  addsproplem5  27887  addsproplem6  27888  sleadd1  27903  addsass  27919  negsid  27954  mulsval  28019  mulsrid  28023  mulsproplem12  28037  mulscom  28049  addsdi  28065  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  onscutlt  28172  ebtwntg  28931  elntg  28933  elrspunsn  33375  bnj553  34881  bnj966  34927  bnj1442  35032  srcmpltd  35063  mrsubrn  35506  elmrsubrn  35513  mvhf  35551  msubvrs  35553  altxpsspw  35971  weiunse  36462  exrecfnlem  37373  matunitlindflem1  37616  poimirlem3  37623  poimirlem31  37651  poimirlem32  37652  mbfresfi  37666  itg2addnclem2  37672  ftc1anclem7  37699  ftc1anc  37701  hdmaplem2N  41771  hdmaplem3  41772  sucidVD  44865  nregmodellem  45010  pimxrneun  45487  mccllem  45598  limcresiooub  45643  limcresioolb  45644  cnrefiisplem  45830  dvmptfprodlem  45945  dvmptfprod  45946  dvnprodlem1  45947  dvnprodlem2  45948  fourierdlem20  46128  fourierdlem38  46146  fourierdlem48  46155  fourierdlem49  46156  fourierdlem51  46158  fourierdlem62  46169  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem71  46178  fouriersw  46232  nnfoctbdjlem  46456  isomenndlem  46531  hoiprodp1  46589  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem4  46599  hspmbllem2  46628  pimrecltpos  46709  setsidel  47380