Theorem elun2 4133

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∪ cun 3897

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  resf1extb  7874  dftpos4  8185  tfrlem11  8317  dif1en  9084  findcard2d  9089  cantnfp1lem1  9585  cantnfp1lem3  9587  tc2  9647  rankunb  9760  rankelun  9782  djurcl  9821  djuss  9830  djuun  9836  dfac2b  10039  cfsmolem  10178  isfin4p1  10223  zornn0g  10413  mnfxr  11187  supxrun  13229  fsumsplitsnun  15676  sumsplit  15689  modfsummodslem1  15713  prmreclem5  16846  acsfiindd  18474  lspsolv  21096  mplcoe1  21990  maducoeval2  22582  restntr  23124  1stckgenlem  23495  fbun  23782  filuni  23827  ufileu  23861  alexsubALTlem4  23992  tmdgsum  24037  icccmplem2  24766  aannenlem2  26291  aalioulem2  26295  noetainflem4  27706  eqscut3  27792  cutlt  27903  addsval  27932  addsrid  27934  addscom  27936  addsproplem4  27942  addsproplem5  27943  addsproplem6  27944  sleadd1  27959  addsass  27975  negsid  28010  mulsval  28078  mulsrid  28082  mulsproplem12  28096  mulscom  28108  addsdi  28124  precsexlem8  28182  precsexlem9  28183  precsexlem11  28185  onscutlt  28232  ebtwntg  29004  elntg  29006  elrspunsn  33459  bnj553  35003  bnj966  35049  bnj1442  35154  srcmpltd  35185  mrsubrn  35656  elmrsubrn  35663  mvhf  35701  msubvrs  35703  altxpsspw  36120  weiunse  36611  exrecfnlem  37523  matunitlindflem1  37756  poimirlem3  37763  poimirlem31  37791  poimirlem32  37792  mbfresfi  37806  itg2addnclem2  37812  ftc1anclem7  37839  ftc1anc  37841  hdmaplem2N  41971  hdmaplem3  41972  sucidVD  45054  nregmodellem  45199  pimxrneun  45674  mccllem  45785  limcresiooub  45828  limcresioolb  45829  cnrefiisplem  46015  dvmptfprodlem  46130  dvmptfprod  46131  dvnprodlem1  46132  dvnprodlem2  46133  fourierdlem20  46313  fourierdlem38  46331  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem62  46354  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem71  46363  fouriersw  46417  nnfoctbdjlem  46641  isomenndlem  46716  hoiprodp1  46774  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  hspmbllem2  46813  pimrecltpos  46894  setsidel  47564