Theorem elun2 4135

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∪ cun 3899

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  resf1extb  7876  dftpos4  8187  tfrlem11  8319  dif1en  9086  findcard2d  9091  cantnfp1lem1  9587  cantnfp1lem3  9589  tc2  9649  rankunb  9762  rankelun  9784  djurcl  9823  djuss  9832  djuun  9838  dfac2b  10041  cfsmolem  10180  isfin4p1  10225  zornn0g  10415  mnfxr  11189  supxrun  13231  fsumsplitsnun  15678  sumsplit  15691  modfsummodslem1  15715  prmreclem5  16848  acsfiindd  18476  lspsolv  21098  mplcoe1  21992  maducoeval2  22584  restntr  23126  1stckgenlem  23497  fbun  23784  filuni  23829  ufileu  23863  alexsubALTlem4  23994  tmdgsum  24039  icccmplem2  24768  aannenlem2  26293  aalioulem2  26297  noetainflem4  27708  eqcuts3  27800  cutlt  27928  addsval  27958  addsrid  27960  addscom  27962  addsproplem4  27968  addsproplem5  27969  addsproplem6  27970  leadds1  27985  addsass  28001  negsid  28037  mulsval  28105  mulsrid  28109  mulsproplem12  28123  mulscom  28135  addsdi  28151  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  oncutlt  28260  ebtwntg  29055  elntg  29057  elrspunsn  33510  bnj553  35054  bnj966  35100  bnj1442  35205  srcmpltd  35236  mrsubrn  35707  elmrsubrn  35714  mvhf  35752  msubvrs  35754  altxpsspw  36171  weiunse  36662  exrecfnlem  37584  matunitlindflem1  37817  poimirlem3  37824  poimirlem31  37852  poimirlem32  37853  mbfresfi  37867  itg2addnclem2  37873  ftc1anclem7  37900  ftc1anc  37902  hdmaplem2N  42032  hdmaplem3  42033  sucidVD  45112  nregmodellem  45257  pimxrneun  45732  mccllem  45843  limcresiooub  45886  limcresioolb  45887  cnrefiisplem  46073  dvmptfprodlem  46188  dvmptfprod  46189  dvnprodlem1  46190  dvnprodlem2  46191  fourierdlem20  46371  fourierdlem38  46389  fourierdlem48  46398  fourierdlem49  46399  fourierdlem51  46401  fourierdlem62  46412  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem71  46421  fouriersw  46475  nnfoctbdjlem  46699  isomenndlem  46774  hoiprodp1  46832  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  hspmbllem2  46871  pimrecltpos  46952  setsidel  47622