Theorem elun2 4142

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

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

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 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  resf1extb  7890  dftpos4  8201  tfrlem11  8333  dif1en  9101  dif1enOLD  9103  findcard2d  9107  cantnfp1lem1  9607  cantnfp1lem3  9609  tc2  9671  rankunb  9779  rankelun  9801  djurcl  9840  djuss  9849  djuun  9855  dfac2b  10060  cfsmolem  10199  isfin4p1  10244  zornn0g  10434  mnfxr  11207  supxrun  13252  fsumsplitsnun  15697  sumsplit  15710  modfsummodslem1  15734  prmreclem5  16867  acsfiindd  18488  lspsolv  21029  mplcoe1  21920  maducoeval2  22503  restntr  23045  1stckgenlem  23416  fbun  23703  filuni  23748  ufileu  23782  alexsubALTlem4  23913  tmdgsum  23958  icccmplem2  24688  aannenlem2  26213  aalioulem2  26217  noetainflem4  27628  cutlt  27816  addsval  27845  addsrid  27847  addscom  27849  addsproplem4  27855  addsproplem5  27856  addsproplem6  27857  sleadd1  27872  addsass  27888  negsid  27923  mulsval  27988  mulsrid  27992  mulsproplem12  28006  mulscom  28018  addsdi  28034  precsexlem8  28092  precsexlem9  28093  precsexlem11  28095  onscutlt  28141  ebtwntg  28885  elntg  28887  elrspunsn  33373  bnj553  34861  bnj966  34907  bnj1442  35012  srcmpltd  35043  mrsubrn  35473  elmrsubrn  35480  mvhf  35518  msubvrs  35520  altxpsspw  35938  weiunse  36429  exrecfnlem  37340  matunitlindflem1  37583  poimirlem3  37590  poimirlem31  37618  poimirlem32  37619  mbfresfi  37633  itg2addnclem2  37639  ftc1anclem7  37666  ftc1anc  37668  hdmaplem2N  41739  hdmaplem3  41740  sucidVD  44834  nregmodellem  44979  pimxrneun  45457  mccllem  45568  limcresiooub  45613  limcresioolb  45614  cnrefiisplem  45800  dvmptfprodlem  45915  dvmptfprod  45916  dvnprodlem1  45917  dvnprodlem2  45918  fourierdlem20  46098  fourierdlem38  46116  fourierdlem48  46125  fourierdlem49  46126  fourierdlem51  46128  fourierdlem62  46139  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem71  46148  fouriersw  46202  nnfoctbdjlem  46426  isomenndlem  46501  hoiprodp1  46559  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  hspmbllem2  46598  pimrecltpos  46679  setsidel  47350