Theorem elun2 4129

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∪ cun 3897

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  srcmpltd  4432  resf1extb  7931  dftpos4  8243  tfrlem11  8377  dif1en  9156  findcard2d  9161  cantnfp1lem1  9657  cantnfp1lem3  9659  tc2  9719  rankunb  9832  rankelun  9854  djurcl  9916  djuss  9925  djuun  9931  dfac2b  10133  cfsmolem  10272  isfin4p1  10317  zornn0g  10507  mnfxr  11290  supxrun  13368  fsumsplitsnun  15841  sumsplit  15854  modfsummodslem1  15879  prmreclem5  17012  acsfiindd  18641  lspsolv  21330  mplcoe1  22253  maducoeval2  22862  matunitlindflem1  22901  restntr  23407  1stckgenlem  23779  fbun  24066  filuni  24111  ufileu  24145  alexsubALTlem4  24276  tmdgsum  24321  icccmplem2  25050  aannenlem2  26565  aalioulem2  26569  noetainflem4  27976  eqcuts3  28069  cutlt  28197  addsval  28227  addsrid  28229  addscom  28231  addsproplem4  28237  addsproplem5  28238  addsproplem6  28239  leadds1  28254  addsass  28270  negsid  28306  mulsval  28374  mulsrid  28378  mulsproplem12  28392  mulscom  28404  addsdi  28420  precsexlem8  28479  precsexlem9  28480  precsexlem11  28482  oncutlt  28529  ebtwntg  29439  elntg  29441  elrspunsn  33857  mplidomlem  34037  bnj553  35407  bnj966  35453  bnj1442  35558  mrsubrn  36092  elmrsubrn  36099  mvhf  36137  msubvrs  36139  altxpsspw  36557  weiunse  37087  exrecfnlem  38133  poimirlem3  38372  poimirlem31  38400  poimirlem32  38401  mbfresfi  38415  itg2addnclem2  38421  ftc1anclem7  38448  ftc1anc  38450  hdmaplem2N  42645  hdmaplem3  42646  sucidVD  45694  nregmodellem  45839  pimxrneun  46316  mccllem  46427  limcresiooub  46470  limcresioolb  46471  cnrefiisplem  46657  dvmptfprodlem  46772  dvmptfprod  46773  dvnprodlem1  46774  dvnprodlem2  46775  fourierdlem20  46955  fourierdlem38  46973  fourierdlem48  46982  fourierdlem49  46983  fourierdlem51  46985  fourierdlem62  46996  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem71  47005  fouriersw  47059  nnfoctbdjlem  47283  isomenndlem  47358  hoiprodp1  47416  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoidmvlelem4  47426  hspmbllem2  47455  pimrecltpos  47536  setsidel  48276