Theorem elun2 4130

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  resf1extb  7864  dftpos4  8175  tfrlem11  8307  dif1en  9071  findcard2d  9076  cantnfp1lem1  9568  cantnfp1lem3  9570  tc2  9630  rankunb  9743  rankelun  9765  djurcl  9804  djuss  9813  djuun  9819  dfac2b  10022  cfsmolem  10161  isfin4p1  10206  zornn0g  10396  mnfxr  11169  supxrun  13215  fsumsplitsnun  15662  sumsplit  15675  modfsummodslem1  15699  prmreclem5  16832  acsfiindd  18459  lspsolv  21080  mplcoe1  21972  maducoeval2  22555  restntr  23097  1stckgenlem  23468  fbun  23755  filuni  23800  ufileu  23834  alexsubALTlem4  23965  tmdgsum  24010  icccmplem2  24739  aannenlem2  26264  aalioulem2  26268  noetainflem4  27679  eqscut3  27765  cutlt  27876  addsval  27905  addsrid  27907  addscom  27909  addsproplem4  27915  addsproplem5  27916  addsproplem6  27917  sleadd1  27932  addsass  27948  negsid  27983  mulsval  28048  mulsrid  28052  mulsproplem12  28066  mulscom  28078  addsdi  28094  precsexlem8  28152  precsexlem9  28153  precsexlem11  28155  onscutlt  28201  ebtwntg  28960  elntg  28962  elrspunsn  33394  bnj553  34910  bnj966  34956  bnj1442  35061  srcmpltd  35092  mrsubrn  35557  elmrsubrn  35564  mvhf  35602  msubvrs  35604  altxpsspw  36019  weiunse  36510  exrecfnlem  37421  matunitlindflem1  37664  poimirlem3  37671  poimirlem31  37699  poimirlem32  37700  mbfresfi  37714  itg2addnclem2  37720  ftc1anclem7  37747  ftc1anc  37749  hdmaplem2N  41819  hdmaplem3  41820  sucidVD  44912  nregmodellem  45057  pimxrneun  45534  mccllem  45645  limcresiooub  45688  limcresioolb  45689  cnrefiisplem  45875  dvmptfprodlem  45990  dvmptfprod  45991  dvnprodlem1  45992  dvnprodlem2  45993  fourierdlem20  46173  fourierdlem38  46191  fourierdlem48  46200  fourierdlem49  46201  fourierdlem51  46203  fourierdlem62  46214  fourierdlem63  46215  fourierdlem64  46216  fourierdlem65  46217  fourierdlem71  46223  fouriersw  46277  nnfoctbdjlem  46501  isomenndlem  46576  hoiprodp1  46634  hoidmvlelem1  46641  hoidmvlelem2  46642  hoidmvlelem3  46643  hoidmvlelem4  46644  hspmbllem2  46673  pimrecltpos  46754  setsidel  47415