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 3933	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2143   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  resf1extb  7927  dftpos4  8237  tfrlem11  8371  dif1en  9142  findcard2d  9147  cantnfp1lem1  9643  cantnfp1lem3  9645  tc2  9705  rankunb  9818  rankelun  9840  djurcl  9893  djuss  9902  djuun  9908  dfac2b  10110  cfsmolem  10249  isfin4p1  10294  zornn0g  10484  mnfxr  11261  supxrun  13337  fsumsplitsnun  15802  sumsplit  15815  modfsummodslem1  15840  prmreclem5  16975  acsfiindd  18604  lspsolv  21267  mplcoe1  22188  maducoeval2  22797  restntr  23339  1stckgenlem  23710  fbun  23997  filuni  24042  ufileu  24076  alexsubALTlem4  24207  tmdgsum  24252  icccmplem2  24981  aannenlem2  26492  aalioulem2  26496  noetainflem4  27904  eqcuts3  27997  cutlt  28125  addsval  28155  addsrid  28157  addscom  28159  addsproplem4  28165  addsproplem5  28166  addsproplem6  28167  leadds1  28182  addsass  28198  negsid  28234  mulsval  28302  mulsrid  28306  mulsproplem12  28320  mulscom  28332  addsdi  28348  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  oncutlt  28457  ebtwntg  29332  elntg  29334  elrspunsn  33737  mplidomlem  33917  bnj553  35286  bnj966  35332  bnj1442  35437  srcmpltd  35469  mrsubrn  36005  elmrsubrn  36012  mvhf  36050  msubvrs  36052  altxpsspw  36469  weiunse  36979  exrecfnlem  38025  matunitlindflem1  38267  poimirlem3  38274  poimirlem31  38302  poimirlem32  38303  mbfresfi  38317  itg2addnclem2  38323  ftc1anclem7  38350  ftc1anc  38352  hdmaplem2N  42546  hdmaplem3  42547  sucidVD  45580  nregmodellem  45725  pimxrneun  46202  mccllem  46313  limcresiooub  46356  limcresioolb  46357  cnrefiisplem  46543  dvmptfprodlem  46658  dvmptfprod  46659  dvnprodlem1  46660  dvnprodlem2  46661  fourierdlem20  46841  fourierdlem38  46859  fourierdlem48  46868  fourierdlem49  46869  fourierdlem51  46871  fourierdlem62  46882  fourierdlem63  46883  fourierdlem64  46884  fourierdlem65  46885  fourierdlem71  46891  fouriersw  46945  nnfoctbdjlem  47169  isomenndlem  47244  hoiprodp1  47302  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  hspmbllem2  47341  pimrecltpos  47422  setsidel  48125