Theorem elun2 4107

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  dftpos4  8032  wfrlem14OLD  8124  tfrlem11  8190  dif1en  8907  findcard2d  8911  cantnfp1lem1  9366  cantnfp1lem3  9368  tc2  9431  rankunb  9539  rankelun  9561  djurcl  9600  djuss  9609  djuun  9615  dfac2b  9817  cfsmolem  9957  isfin4p1  10002  zornn0g  10192  mnfxr  10963  supxrun  12979  fsumsplitsnun  15395  sumsplit  15408  modfsummodslem1  15432  prmreclem5  16549  acsfiindd  18186  lspsolv  20320  mplcoe1  21148  maducoeval2  21697  restntr  22241  1stckgenlem  22612  fbun  22899  filuni  22944  ufileu  22978  alexsubALTlem4  23109  tmdgsum  23154  icccmplem2  23892  aannenlem2  25394  aalioulem2  25398  ebtwntg  27253  elntg  27255  bnj553  32778  bnj966  32824  bnj1442  32929  srcmpltd  32954  mrsubrn  33375  elmrsubrn  33382  mvhf  33420  msubvrs  33422  noetainflem4  33870  addsval  34053  addsid1  34054  addscom  34056  altxpsspw  34206  exrecfnlem  35477  matunitlindflem1  35700  poimirlem3  35707  poimirlem31  35735  poimirlem32  35736  mbfresfi  35750  itg2addnclem2  35756  ftc1anclem7  35783  ftc1anc  35785  hdmaplem2N  39713  hdmaplem3  39714  metakunt22  40074  sucidVD  42381  mccllem  43028  limcresiooub  43073  limcresioolb  43074  cnrefiisplem  43260  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem1  43377  dvnprodlem2  43378  fourierdlem20  43558  fourierdlem38  43576  fourierdlem48  43585  fourierdlem49  43586  fourierdlem51  43588  fourierdlem62  43599  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem71  43608  fouriersw  43662  nnfoctbdjlem  43883  isomenndlem  43958  hoiprodp1  44016  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hspmbllem2  44055  pimrecltpos  44133  setsidel  44716