Theorem elun2 4144

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  resf1extb  7930  dftpos4  8240  tfrlem11  8374  dif1en  9145  findcard2d  9150  cantnfp1lem1  9646  cantnfp1lem3  9648  tc2  9708  rankunb  9821  rankelun  9843  djurcl  9896  djuss  9905  djuun  9911  dfac2b  10113  cfsmolem  10253  isfin4p1  10298  zornn0g  10488  mnfxr  11265  supxrun  13341  fsumsplitsnun  15805  sumsplit  15818  modfsummodslem1  15843  prmreclem5  16979  acsfiindd  18608  lspsolv  21244  mplcoe1  22156  maducoeval2  22765  restntr  23307  1stckgenlem  23678  fbun  23965  filuni  24010  ufileu  24044  alexsubALTlem4  24175  tmdgsum  24220  icccmplem2  24949  aannenlem2  26458  aalioulem2  26462  noetainflem4  27869  eqcuts3  27962  cutlt  28090  addsval  28120  addsrid  28122  addscom  28124  addsproplem4  28130  addsproplem5  28131  addsproplem6  28132  leadds1  28147  addsass  28163  negsid  28199  mulsval  28267  mulsrid  28271  mulsproplem12  28285  mulscom  28297  addsdi  28313  precsexlem8  28372  precsexlem9  28373  precsexlem11  28375  oncutlt  28422  ebtwntg  29272  elntg  29274  elrspunsn  33680  mplidomlem  33861  bnj553  35230  bnj966  35276  bnj1442  35381  srcmpltd  35412  mrsubrn  35903  elmrsubrn  35910  mvhf  35948  msubvrs  35950  altxpsspw  36367  weiunse  36867  exrecfnlem  37912  matunitlindflem1  38154  poimirlem3  38161  poimirlem31  38189  poimirlem32  38190  mbfresfi  38204  itg2addnclem2  38210  ftc1anclem7  38237  ftc1anc  38239  hdmaplem2N  42435  hdmaplem3  42436  sucidVD  45471  nregmodellem  45616  pimxrneun  46093  mccllem  46204  limcresiooub  46247  limcresioolb  46248  cnrefiisplem  46434  dvmptfprodlem  46549  dvmptfprod  46550  dvnprodlem1  46551  dvnprodlem2  46552  fourierdlem20  46732  fourierdlem38  46750  fourierdlem48  46759  fourierdlem49  46760  fourierdlem51  46762  fourierdlem62  46773  fourierdlem63  46774  fourierdlem64  46775  fourierdlem65  46776  fourierdlem71  46782  fouriersw  46836  nnfoctbdjlem  47060  isomenndlem  47135  hoiprodp1  47193  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem4  47203  hspmbllem2  47232  pimrecltpos  47313  setsidel  48013