Theorem elun2 4111

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  dftpos4  8061  wfrlem14OLD  8153  tfrlem11  8219  dif1en  8945  findcard2d  8949  cantnfp1lem1  9436  cantnfp1lem3  9438  tc2  9500  rankunb  9608  rankelun  9630  djurcl  9669  djuss  9678  djuun  9684  dfac2b  9886  cfsmolem  10026  isfin4p1  10071  zornn0g  10261  mnfxr  11032  supxrun  13050  fsumsplitsnun  15467  sumsplit  15480  modfsummodslem1  15504  prmreclem5  16621  acsfiindd  18271  lspsolv  20405  mplcoe1  21238  maducoeval2  21789  restntr  22333  1stckgenlem  22704  fbun  22991  filuni  23036  ufileu  23070  alexsubALTlem4  23201  tmdgsum  23246  icccmplem2  23986  aannenlem2  25489  aalioulem2  25493  ebtwntg  27350  elntg  27352  bnj553  32878  bnj966  32924  bnj1442  33029  srcmpltd  33054  mrsubrn  33475  elmrsubrn  33482  mvhf  33520  msubvrs  33522  noetainflem4  33943  addsval  34126  addsid1  34127  addscom  34129  altxpsspw  34279  exrecfnlem  35550  matunitlindflem1  35773  poimirlem3  35780  poimirlem31  35808  poimirlem32  35809  mbfresfi  35823  itg2addnclem2  35829  ftc1anclem7  35856  ftc1anc  35858  hdmaplem2N  39786  hdmaplem3  39787  metakunt22  40146  sucidVD  42492  mccllem  43138  limcresiooub  43183  limcresioolb  43184  cnrefiisplem  43370  dvmptfprodlem  43485  dvmptfprod  43486  dvnprodlem1  43487  dvnprodlem2  43488  fourierdlem20  43668  fourierdlem38  43686  fourierdlem48  43695  fourierdlem49  43696  fourierdlem51  43698  fourierdlem62  43709  fourierdlem63  43710  fourierdlem64  43711  fourierdlem65  43712  fourierdlem71  43718  fouriersw  43772  nnfoctbdjlem  43993  isomenndlem  44068  hoiprodp1  44126  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  hspmbllem2  44165  pimrecltpos  44245  setsidel  44828