Theorem elun2 4136

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∪ cun 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  srcmpltd  4439  resf1extb  7937  dftpos4  8247  tfrlem11  8381  dif1en  9153  findcard2d  9158  cantnfp1lem1  9654  cantnfp1lem3  9656  tc2  9716  rankunb  9829  rankelun  9851  djurcl  9913  djuss  9922  djuun  9928  dfac2b  10130  cfsmolem  10269  isfin4p1  10314  zornn0g  10504  mnfxr  11281  supxrun  13358  fsumsplitsnun  15829  sumsplit  15842  modfsummodslem1  15867  prmreclem5  17002  acsfiindd  18631  lspsolv  21317  mplcoe1  22238  maducoeval2  22847  restntr  23389  1stckgenlem  23761  fbun  24048  filuni  24093  ufileu  24127  alexsubALTlem4  24258  tmdgsum  24303  icccmplem2  25032  aannenlem2  26543  aalioulem2  26547  noetainflem4  27955  eqcuts3  28048  cutlt  28176  addsval  28206  addsrid  28208  addscom  28210  addsproplem4  28216  addsproplem5  28217  addsproplem6  28218  leadds1  28233  addsass  28249  negsid  28285  mulsval  28353  mulsrid  28357  mulsproplem12  28371  mulscom  28383  addsdi  28399  precsexlem8  28458  precsexlem9  28459  precsexlem11  28461  oncutlt  28508  ebtwntg  29387  elntg  29389  elrspunsn  33801  mplidomlem  33981  bnj553  35351  bnj966  35397  bnj1442  35502  mrsubrn  36042  elmrsubrn  36049  mvhf  36087  msubvrs  36089  altxpsspw  36506  weiunse  37036  exrecfnlem  38082  matunitlindflem1  38324  poimirlem3  38331  poimirlem31  38359  poimirlem32  38360  mbfresfi  38374  itg2addnclem2  38380  ftc1anclem7  38407  ftc1anc  38409  hdmaplem2N  42604  hdmaplem3  42605  sucidVD  45638  nregmodellem  45783  pimxrneun  46260  mccllem  46371  limcresiooub  46414  limcresioolb  46415  cnrefiisplem  46601  dvmptfprodlem  46716  dvmptfprod  46717  dvnprodlem1  46718  dvnprodlem2  46719  fourierdlem20  46899  fourierdlem38  46917  fourierdlem48  46926  fourierdlem49  46927  fourierdlem51  46929  fourierdlem62  46940  fourierdlem63  46941  fourierdlem64  46942  fourierdlem65  46943  fourierdlem71  46949  fouriersw  47003  nnfoctbdjlem  47227  isomenndlem  47302  hoiprodp1  47360  hoidmvlelem1  47367  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem4  47370  hspmbllem2  47399  pimrecltpos  47480  setsidel  48183