Theorem elun2 4206

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  dftpos4  8286  wfrlem14OLD  8378  tfrlem11  8444  dif1en  9226  dif1enOLD  9228  findcard2d  9232  cantnfp1lem1  9747  cantnfp1lem3  9749  tc2  9811  rankunb  9919  rankelun  9941  djurcl  9980  djuss  9989  djuun  9995  dfac2b  10200  cfsmolem  10339  isfin4p1  10384  zornn0g  10574  mnfxr  11347  supxrun  13378  fsumsplitsnun  15803  sumsplit  15816  modfsummodslem1  15840  prmreclem5  16967  acsfiindd  18623  lspsolv  21168  mplcoe1  22078  maducoeval2  22667  restntr  23211  1stckgenlem  23582  fbun  23869  filuni  23914  ufileu  23948  alexsubALTlem4  24079  tmdgsum  24124  icccmplem2  24864  aannenlem2  26389  aalioulem2  26393  noetainflem4  27803  cutlt  27984  addsval  28013  addsrid  28015  addscom  28017  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  sleadd1  28040  addsass  28056  negsid  28091  mulsval  28153  mulsrid  28157  mulsproplem12  28171  mulscom  28183  addsdi  28199  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  ebtwntg  29015  elntg  29017  elrspunsn  33422  bnj553  34874  bnj966  34920  bnj1442  35025  srcmpltd  35056  mrsubrn  35481  elmrsubrn  35488  mvhf  35526  msubvrs  35528  altxpsspw  35941  weiunse  36434  exrecfnlem  37345  matunitlindflem1  37576  poimirlem3  37583  poimirlem31  37611  poimirlem32  37612  mbfresfi  37626  itg2addnclem2  37632  ftc1anclem7  37659  ftc1anc  37661  hdmaplem2N  41729  hdmaplem3  41730  metakunt22  42183  sucidVD  44843  pimxrneun  45404  mccllem  45518  limcresiooub  45563  limcresioolb  45564  cnrefiisplem  45750  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem1  45867  dvnprodlem2  45868  fourierdlem20  46048  fourierdlem38  46066  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem62  46089  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem71  46098  fouriersw  46152  nnfoctbdjlem  46376  isomenndlem  46451  hoiprodp1  46509  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hspmbllem2  46548  pimrecltpos  46629  setsidel  47250