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  18494  lspsolv  21085  mplcoe1  21977  maducoeval2  22560  restntr  23102  1stckgenlem  23473  fbun  23760  filuni  23805  ufileu  23839  alexsubALTlem4  23970  tmdgsum  24015  icccmplem2  24745  aannenlem2  26270  aalioulem2  26274  noetainflem4  27685  eqscut3  27770  cutlt  27880  addsval  27909  addsrid  27911  addscom  27913  addsproplem4  27919  addsproplem5  27920  addsproplem6  27921  sleadd1  27936  addsass  27952  negsid  27987  mulsval  28052  mulsrid  28056  mulsproplem12  28070  mulscom  28082  addsdi  28098  precsexlem8  28156  precsexlem9  28157  precsexlem11  28159  onscutlt  28205  ebtwntg  28962  elntg  28964  elrspunsn  33393  bnj553  34881  bnj966  34927  bnj1442  35032  srcmpltd  35063  mrsubrn  35493  elmrsubrn  35500  mvhf  35538  msubvrs  35540  altxpsspw  35958  weiunse  36449  exrecfnlem  37360  matunitlindflem1  37603  poimirlem3  37610  poimirlem31  37638  poimirlem32  37639  mbfresfi  37653  itg2addnclem2  37659  ftc1anclem7  37686  ftc1anc  37688  hdmaplem2N  41759  hdmaplem3  41760  sucidVD  44854  nregmodellem  44999  pimxrneun  45477  mccllem  45588  limcresiooub  45633  limcresioolb  45634  cnrefiisplem  45820  dvmptfprodlem  45935  dvmptfprod  45936  dvnprodlem1  45937  dvnprodlem2  45938  fourierdlem20  46118  fourierdlem38  46136  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem62  46159  fourierdlem63  46160  fourierdlem64  46161  fourierdlem65  46162  fourierdlem71  46168  fouriersw  46222  nnfoctbdjlem  46446  isomenndlem  46521  hoiprodp1  46579  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  hspmbllem2  46618  pimrecltpos  46699  setsidel  47370