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  27735  cutlt  27845  addsval  27874  addsrid  27876  addscom  27878  addsproplem4  27884  addsproplem5  27885  addsproplem6  27886  sleadd1  27901  addsass  27917  negsid  27952  mulsval  28017  mulsrid  28021  mulsproplem12  28035  mulscom  28047  addsdi  28063  precsexlem8  28121  precsexlem9  28122  precsexlem11  28124  onscutlt  28170  ebtwntg  28927  elntg  28929  elrspunsn  33366  bnj553  34865  bnj966  34911  bnj1442  35016  srcmpltd  35047  mrsubrn  35486  elmrsubrn  35493  mvhf  35531  msubvrs  35533  altxpsspw  35951  weiunse  36442  exrecfnlem  37353  matunitlindflem1  37596  poimirlem3  37603  poimirlem31  37631  poimirlem32  37632  mbfresfi  37646  itg2addnclem2  37652  ftc1anclem7  37679  ftc1anc  37681  hdmaplem2N  41751  hdmaplem3  41752  sucidVD  44845  nregmodellem  44990  pimxrneun  45467  mccllem  45578  limcresiooub  45623  limcresioolb  45624  cnrefiisplem  45810  dvmptfprodlem  45925  dvmptfprod  45926  dvnprodlem1  45927  dvnprodlem2  45928  fourierdlem20  46108  fourierdlem38  46126  fourierdlem48  46135  fourierdlem49  46136  fourierdlem51  46138  fourierdlem62  46149  fourierdlem63  46150  fourierdlem64  46151  fourierdlem65  46152  fourierdlem71  46158  fouriersw  46212  nnfoctbdjlem  46436  isomenndlem  46511  hoiprodp1  46569  hoidmvlelem1  46576  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  hspmbllem2  46608  pimrecltpos  46689  setsidel  47360