Theorem elun2 4144

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  resf1extb  7931  dftpos4  8241  tfrlem11  8375  dif1en  9146  findcard2d  9151  cantnfp1lem1  9647  cantnfp1lem3  9649  tc2  9709  rankunb  9822  rankelun  9844  djurcl  9897  djuss  9906  djuun  9912  dfac2b  10114  cfsmolem  10254  isfin4p1  10299  zornn0g  10489  mnfxr  11266  supxrun  13342  fsumsplitsnun  15806  sumsplit  15819  modfsummodslem1  15844  prmreclem5  16980  acsfiindd  18609  lspsolv  21245  mplcoe1  22157  maducoeval2  22766  restntr  23308  1stckgenlem  23679  fbun  23966  filuni  24011  ufileu  24045  alexsubALTlem4  24176  tmdgsum  24221  icccmplem2  24950  aannenlem2  26459  aalioulem2  26463  noetainflem4  27870  eqcuts3  27963  cutlt  28091  addsval  28121  addsrid  28123  addscom  28125  addsproplem4  28131  addsproplem5  28132  addsproplem6  28133  leadds1  28148  addsass  28164  negsid  28200  mulsval  28268  mulsrid  28272  mulsproplem12  28286  mulscom  28298  addsdi  28314  precsexlem8  28373  precsexlem9  28374  precsexlem11  28376  oncutlt  28423  ebtwntg  29273  elntg  29275  elrspunsn  33681  mplidomlem  33862  bnj553  35231  bnj966  35277  bnj1442  35382  srcmpltd  35413  mrsubrn  35938  elmrsubrn  35945  mvhf  35983  msubvrs  35985  altxpsspw  36402  weiunse  36902  exrecfnlem  37947  matunitlindflem1  38189  poimirlem3  38196  poimirlem31  38224  poimirlem32  38225  mbfresfi  38239  itg2addnclem2  38245  ftc1anclem7  38272  ftc1anc  38274  hdmaplem2N  42470  hdmaplem3  42471  sucidVD  45506  nregmodellem  45651  pimxrneun  46128  mccllem  46239  limcresiooub  46282  limcresioolb  46283  cnrefiisplem  46469  dvmptfprodlem  46584  dvmptfprod  46585  dvnprodlem1  46586  dvnprodlem2  46587  fourierdlem20  46767  fourierdlem38  46785  fourierdlem48  46794  fourierdlem49  46795  fourierdlem51  46797  fourierdlem62  46808  fourierdlem63  46809  fourierdlem64  46810  fourierdlem65  46811  fourierdlem71  46817  fouriersw  46871  nnfoctbdjlem  47095  isomenndlem  47170  hoiprodp1  47228  hoidmvlelem1  47235  hoidmvlelem2  47236  hoidmvlelem3  47237  hoidmvlelem4  47238  hspmbllem2  47267  pimrecltpos  47348  setsidel  48048