Theorem elun2 4177

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∪ cun 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  dftpos4  8229  wfrlem14OLD  8321  tfrlem11  8387  dif1en  9159  dif1enOLD  9161  findcard2d  9165  cantnfp1lem1  9672  cantnfp1lem3  9674  tc2  9736  rankunb  9844  rankelun  9866  djurcl  9905  djuss  9914  djuun  9920  dfac2b  10124  cfsmolem  10264  isfin4p1  10309  zornn0g  10499  mnfxr  11270  supxrun  13294  fsumsplitsnun  15700  sumsplit  15713  modfsummodslem1  15737  prmreclem5  16852  acsfiindd  18505  lspsolv  20755  mplcoe1  21591  maducoeval2  22141  restntr  22685  1stckgenlem  23056  fbun  23343  filuni  23388  ufileu  23422  alexsubALTlem4  23553  tmdgsum  23598  icccmplem2  24338  aannenlem2  25841  aalioulem2  25845  noetainflem4  27240  cutlt  27416  addsval  27443  addsrid  27445  addscom  27447  addsproplem4  27453  addsproplem5  27454  addsproplem6  27455  sleadd1  27469  addsass  27485  negsid  27512  mulsval  27562  mulsrid  27566  mulsproplem12  27580  mulscom  27592  addsdi  27607  precsexlem8  27657  precsexlem9  27658  precsexlem11  27660  ebtwntg  28237  elntg  28239  elrspunsn  32542  bnj553  33904  bnj966  33950  bnj1442  34055  srcmpltd  34080  mrsubrn  34499  elmrsubrn  34506  mvhf  34544  msubvrs  34546  altxpsspw  34944  exrecfnlem  36255  matunitlindflem1  36479  poimirlem3  36486  poimirlem31  36514  poimirlem32  36515  mbfresfi  36529  itg2addnclem2  36535  ftc1anclem7  36562  ftc1anc  36564  hdmaplem2N  40638  hdmaplem3  40639  metakunt22  41001  sucidVD  43623  pimxrneun  44189  mccllem  44303  limcresiooub  44348  limcresioolb  44349  cnrefiisplem  44535  dvmptfprodlem  44650  dvmptfprod  44651  dvnprodlem1  44652  dvnprodlem2  44653  fourierdlem20  44833  fourierdlem38  44851  fourierdlem48  44860  fourierdlem49  44861  fourierdlem51  44863  fourierdlem62  44874  fourierdlem63  44875  fourierdlem64  44876  fourierdlem65  44877  fourierdlem71  44883  fouriersw  44937  nnfoctbdjlem  45161  isomenndlem  45236  hoiprodp1  45294  hoidmvlelem1  45301  hoidmvlelem2  45302  hoidmvlelem3  45303  hoidmvlelem4  45304  hspmbllem2  45333  pimrecltpos  45414  setsidel  46034