Theorem elun2 4146

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  resf1extb  7910  dftpos4  8224  tfrlem11  8356  dif1en  9124  dif1enOLD  9126  findcard2d  9130  cantnfp1lem1  9631  cantnfp1lem3  9633  tc2  9695  rankunb  9803  rankelun  9825  djurcl  9864  djuss  9873  djuun  9879  dfac2b  10084  cfsmolem  10223  isfin4p1  10268  zornn0g  10458  mnfxr  11231  supxrun  13276  fsumsplitsnun  15721  sumsplit  15734  modfsummodslem1  15758  prmreclem5  16891  acsfiindd  18512  lspsolv  21053  mplcoe1  21944  maducoeval2  22527  restntr  23069  1stckgenlem  23440  fbun  23727  filuni  23772  ufileu  23806  alexsubALTlem4  23937  tmdgsum  23982  icccmplem2  24712  aannenlem2  26237  aalioulem2  26241  noetainflem4  27652  cutlt  27840  addsval  27869  addsrid  27871  addscom  27873  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  sleadd1  27896  addsass  27912  negsid  27947  mulsval  28012  mulsrid  28016  mulsproplem12  28030  mulscom  28042  addsdi  28058  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  onscutlt  28165  ebtwntg  28909  elntg  28911  elrspunsn  33400  bnj553  34888  bnj966  34934  bnj1442  35039  srcmpltd  35070  mrsubrn  35500  elmrsubrn  35507  mvhf  35545  msubvrs  35547  altxpsspw  35965  weiunse  36456  exrecfnlem  37367  matunitlindflem1  37610  poimirlem3  37617  poimirlem31  37645  poimirlem32  37646  mbfresfi  37660  itg2addnclem2  37666  ftc1anclem7  37693  ftc1anc  37695  hdmaplem2N  41766  hdmaplem3  41767  sucidVD  44861  nregmodellem  45006  pimxrneun  45484  mccllem  45595  limcresiooub  45640  limcresioolb  45641  cnrefiisplem  45827  dvmptfprodlem  45942  dvmptfprod  45943  dvnprodlem1  45944  dvnprodlem2  45945  fourierdlem20  46125  fourierdlem38  46143  fourierdlem48  46152  fourierdlem49  46153  fourierdlem51  46155  fourierdlem62  46166  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem71  46175  fouriersw  46229  nnfoctbdjlem  46453  isomenndlem  46528  hoiprodp1  46586  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hspmbllem2  46625  pimrecltpos  46706  setsidel  47377