Theorem elun2 4137

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  resf1extb  7886  dftpos4  8197  tfrlem11  8329  dif1en  9098  findcard2d  9103  cantnfp1lem1  9599  cantnfp1lem3  9601  tc2  9661  rankunb  9774  rankelun  9796  djurcl  9835  djuss  9844  djuun  9850  dfac2b  10053  cfsmolem  10192  isfin4p1  10237  zornn0g  10427  mnfxr  11201  supxrun  13243  fsumsplitsnun  15690  sumsplit  15703  modfsummodslem1  15727  prmreclem5  16860  acsfiindd  18488  lspsolv  21110  mplcoe1  22004  maducoeval2  22596  restntr  23138  1stckgenlem  23509  fbun  23796  filuni  23841  ufileu  23875  alexsubALTlem4  24006  tmdgsum  24051  icccmplem2  24780  aannenlem2  26305  aalioulem2  26309  noetainflem4  27720  eqcuts3  27812  cutlt  27940  addsval  27970  addsrid  27972  addscom  27974  addsproplem4  27980  addsproplem5  27981  addsproplem6  27982  leadds1  27997  addsass  28013  negsid  28049  mulsval  28117  mulsrid  28121  mulsproplem12  28135  mulscom  28147  addsdi  28163  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  oncutlt  28272  ebtwntg  29067  elntg  29069  elrspunsn  33522  bnj553  35074  bnj966  35120  bnj1442  35225  srcmpltd  35256  mrsubrn  35729  elmrsubrn  35736  mvhf  35774  msubvrs  35776  altxpsspw  36193  weiunse  36684  exrecfnlem  37634  matunitlindflem1  37867  poimirlem3  37874  poimirlem31  37902  poimirlem32  37903  mbfresfi  37917  itg2addnclem2  37923  ftc1anclem7  37950  ftc1anc  37952  hdmaplem2N  42148  hdmaplem3  42149  sucidVD  45227  nregmodellem  45372  pimxrneun  45846  mccllem  45957  limcresiooub  46000  limcresioolb  46001  cnrefiisplem  46187  dvmptfprodlem  46302  dvmptfprod  46303  dvnprodlem1  46304  dvnprodlem2  46305  fourierdlem20  46485  fourierdlem38  46503  fourierdlem48  46512  fourierdlem49  46513  fourierdlem51  46515  fourierdlem62  46526  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem71  46535  fouriersw  46589  nnfoctbdjlem  46813  isomenndlem  46888  hoiprodp1  46946  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  hspmbllem2  46985  pimrecltpos  47066  setsidel  47736