Theorem elun2 4112

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

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

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-un 3893  df-in 3895  df-ss 3905

This theorem is referenced by:  dftpos4  8050  wfrlem14OLD  8142  tfrlem11  8208  dif1en  8934  findcard2d  8938  cantnfp1lem1  9425  cantnfp1lem3  9427  tc2  9489  rankunb  9597  rankelun  9619  djurcl  9658  djuss  9667  djuun  9673  dfac2b  9875  cfsmolem  10015  isfin4p1  10060  zornn0g  10250  mnfxr  11021  supxrun  13039  fsumsplitsnun  15456  sumsplit  15469  modfsummodslem1  15493  prmreclem5  16610  acsfiindd  18260  lspsolv  20394  mplcoe1  21227  maducoeval2  21778  restntr  22322  1stckgenlem  22693  fbun  22980  filuni  23025  ufileu  23059  alexsubALTlem4  23190  tmdgsum  23235  icccmplem2  23975  aannenlem2  25478  aalioulem2  25482  ebtwntg  27339  elntg  27341  bnj553  32865  bnj966  32911  bnj1442  33016  srcmpltd  33041  mrsubrn  33462  elmrsubrn  33469  mvhf  33507  msubvrs  33509  noetainflem4  33930  addsval  34113  addsid1  34114  addscom  34116  altxpsspw  34266  exrecfnlem  35537  matunitlindflem1  35760  poimirlem3  35767  poimirlem31  35795  poimirlem32  35796  mbfresfi  35810  itg2addnclem2  35816  ftc1anclem7  35843  ftc1anc  35845  hdmaplem2N  39773  hdmaplem3  39774  metakunt22  40133  sucidVD  42452  mccllem  43098  limcresiooub  43143  limcresioolb  43144  cnrefiisplem  43330  dvmptfprodlem  43445  dvmptfprod  43446  dvnprodlem1  43447  dvnprodlem2  43448  fourierdlem20  43628  fourierdlem38  43646  fourierdlem48  43655  fourierdlem49  43656  fourierdlem51  43658  fourierdlem62  43669  fourierdlem63  43670  fourierdlem64  43671  fourierdlem65  43672  fourierdlem71  43678  fouriersw  43732  nnfoctbdjlem  43953  isomenndlem  44028  hoiprodp1  44086  hoidmvlelem1  44093  hoidmvlelem2  44094  hoidmvlelem3  44095  hoidmvlelem4  44096  hspmbllem2  44125  pimrecltpos  44203  setsidel  44785