Theorem elun2 4178

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  dftpos4  8230  wfrlem14OLD  8322  tfrlem11  8388  dif1en  9160  dif1enOLD  9162  findcard2d  9166  cantnfp1lem1  9673  cantnfp1lem3  9675  tc2  9737  rankunb  9845  rankelun  9867  djurcl  9906  djuss  9915  djuun  9921  dfac2b  10125  cfsmolem  10265  isfin4p1  10310  zornn0g  10500  mnfxr  11271  supxrun  13295  fsumsplitsnun  15701  sumsplit  15714  modfsummodslem1  15738  prmreclem5  16853  acsfiindd  18506  lspsolv  20756  mplcoe1  21592  maducoeval2  22142  restntr  22686  1stckgenlem  23057  fbun  23344  filuni  23389  ufileu  23423  alexsubALTlem4  23554  tmdgsum  23599  icccmplem2  24339  aannenlem2  25842  aalioulem2  25846  noetainflem4  27243  cutlt  27419  addsval  27446  addsrid  27448  addscom  27450  addsproplem4  27456  addsproplem5  27457  addsproplem6  27458  sleadd1  27472  addsass  27488  negsid  27515  mulsval  27565  mulsrid  27569  mulsproplem12  27583  mulscom  27595  addsdi  27610  precsexlem8  27660  precsexlem9  27661  precsexlem11  27663  ebtwntg  28240  elntg  28242  elrspunsn  32547  bnj553  33909  bnj966  33955  bnj1442  34060  srcmpltd  34085  mrsubrn  34504  elmrsubrn  34511  mvhf  34549  msubvrs  34551  altxpsspw  34949  exrecfnlem  36260  matunitlindflem1  36484  poimirlem3  36491  poimirlem31  36519  poimirlem32  36520  mbfresfi  36534  itg2addnclem2  36540  ftc1anclem7  36567  ftc1anc  36569  hdmaplem2N  40643  hdmaplem3  40644  metakunt22  41006  sucidVD  43633  pimxrneun  44199  mccllem  44313  limcresiooub  44358  limcresioolb  44359  cnrefiisplem  44545  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem1  44662  dvnprodlem2  44663  fourierdlem20  44843  fourierdlem38  44861  fourierdlem48  44870  fourierdlem49  44871  fourierdlem51  44873  fourierdlem62  44884  fourierdlem63  44885  fourierdlem64  44886  fourierdlem65  44887  fourierdlem71  44893  fouriersw  44947  nnfoctbdjlem  45171  isomenndlem  45246  hoiprodp1  45304  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  hspmbllem2  45343  pimrecltpos  45424  setsidel  46044