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 2105   ∪ cun 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  dftpos4  8236  wfrlem14OLD  8328  tfrlem11  8394  dif1en  9166  dif1enOLD  9168  findcard2d  9172  cantnfp1lem1  9679  cantnfp1lem3  9681  tc2  9743  rankunb  9851  rankelun  9873  djurcl  9912  djuss  9921  djuun  9927  dfac2b  10131  cfsmolem  10271  isfin4p1  10316  zornn0g  10506  mnfxr  11278  supxrun  13302  fsumsplitsnun  15708  sumsplit  15721  modfsummodslem1  15745  prmreclem5  16860  acsfiindd  18516  lspsolv  20990  mplcoe1  21903  maducoeval2  22462  restntr  23006  1stckgenlem  23377  fbun  23664  filuni  23709  ufileu  23743  alexsubALTlem4  23874  tmdgsum  23919  icccmplem2  24659  aannenlem2  26181  aalioulem2  26185  noetainflem4  27586  cutlt  27765  addsval  27792  addsrid  27794  addscom  27796  addsproplem4  27802  addsproplem5  27803  addsproplem6  27804  sleadd1  27819  addsass  27835  negsid  27866  mulsval  27922  mulsrid  27926  mulsproplem12  27940  mulscom  27952  addsdi  27968  precsexlem8  28025  precsexlem9  28026  precsexlem11  28028  ebtwntg  28673  elntg  28675  elrspunsn  32987  bnj553  34373  bnj966  34419  bnj1442  34524  srcmpltd  34549  mrsubrn  34968  elmrsubrn  34975  mvhf  35013  msubvrs  35015  altxpsspw  35419  exrecfnlem  36724  matunitlindflem1  36948  poimirlem3  36955  poimirlem31  36983  poimirlem32  36984  mbfresfi  36998  itg2addnclem2  37004  ftc1anclem7  37031  ftc1anc  37033  hdmaplem2N  41107  hdmaplem3  41108  metakunt22  41473  sucidVD  44096  pimxrneun  44658  mccllem  44772  limcresiooub  44817  limcresioolb  44818  cnrefiisplem  45004  dvmptfprodlem  45119  dvmptfprod  45120  dvnprodlem1  45121  dvnprodlem2  45122  fourierdlem20  45302  fourierdlem38  45320  fourierdlem48  45329  fourierdlem49  45330  fourierdlem51  45332  fourierdlem62  45343  fourierdlem63  45344  fourierdlem64  45345  fourierdlem65  45346  fourierdlem71  45352  fouriersw  45406  nnfoctbdjlem  45630  isomenndlem  45705  hoiprodp1  45763  hoidmvlelem1  45770  hoidmvlelem2  45771  hoidmvlelem3  45772  hoidmvlelem4  45773  hspmbllem2  45802  pimrecltpos  45883  setsidel  46503