Theorem elun2 4124

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  resf1extb  7879  dftpos4  8189  tfrlem11  8321  dif1en  9090  findcard2d  9095  cantnfp1lem1  9593  cantnfp1lem3  9595  tc2  9655  rankunb  9768  rankelun  9790  djurcl  9829  djuss  9838  djuun  9844  dfac2b  10047  cfsmolem  10186  isfin4p1  10231  zornn0g  10421  mnfxr  11196  supxrun  13262  fsumsplitsnun  15711  sumsplit  15724  modfsummodslem1  15749  prmreclem5  16885  acsfiindd  18513  lspsolv  21136  mplcoe1  22028  maducoeval2  22618  restntr  23160  1stckgenlem  23531  fbun  23818  filuni  23863  ufileu  23897  alexsubALTlem4  24028  tmdgsum  24073  icccmplem2  24802  aannenlem2  26309  aalioulem2  26313  noetainflem4  27721  eqcuts3  27813  cutlt  27941  addsval  27971  addsrid  27973  addscom  27975  addsproplem4  27981  addsproplem5  27982  addsproplem6  27983  leadds1  27998  addsass  28014  negsid  28050  mulsval  28118  mulsrid  28122  mulsproplem12  28136  mulscom  28148  addsdi  28164  precsexlem8  28223  precsexlem9  28224  precsexlem11  28226  oncutlt  28273  ebtwntg  29068  elntg  29070  elrspunsn  33507  bnj553  35059  bnj966  35105  bnj1442  35210  srcmpltd  35241  mrsubrn  35714  elmrsubrn  35721  mvhf  35759  msubvrs  35761  altxpsspw  36178  weiunse  36669  exrecfnlem  37712  matunitlindflem1  37954  poimirlem3  37961  poimirlem31  37989  poimirlem32  37990  mbfresfi  38004  itg2addnclem2  38010  ftc1anclem7  38037  ftc1anc  38039  hdmaplem2N  42235  hdmaplem3  42236  sucidVD  45319  nregmodellem  45464  pimxrneun  45937  mccllem  46048  limcresiooub  46091  limcresioolb  46092  cnrefiisplem  46278  dvmptfprodlem  46393  dvmptfprod  46394  dvnprodlem1  46395  dvnprodlem2  46396  fourierdlem20  46576  fourierdlem38  46594  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem62  46617  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem71  46626  fouriersw  46680  nnfoctbdjlem  46904  isomenndlem  46979  hoiprodp1  47037  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  hspmbllem2  47076  pimrecltpos  47157  setsidel  47851