Theorem elun2 3781

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

Syntax hints:   → wi 4   ∈ wcel 1990   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  dftpos4  7371  wfrlem14  7428  tfrlem11  7484  findcard2d  8202  cantnfp1lem1  8575  cantnfp1lem3  8577  tc2  8618  rankunb  8713  rankelun  8735  dfac2  8953  cfsmolem  9092  isfin4-3  9137  zornn0g  9327  mnfxr  10096  supxrun  12146  fsumsplitsnun  14484  fsumsplitsnunOLD  14486  sumsplit  14499  modfsummodslem1  14524  prmreclem5  15624  acsfiindd  17177  lspsolv  19143  mplcoe1  19465  maducoeval2  20446  restntr  20986  1stckgenlem  21356  fbun  21644  filuni  21689  ufileu  21723  alexsubALTlem4  21854  tmdgsum  21899  icccmplem2  22626  aannenlem2  24084  aalioulem2  24088  ebtwntg  25862  elntg  25864  bnj553  30968  bnj966  31014  bnj1442  31117  mrsubrn  31410  elmrsubrn  31417  mvhf  31455  msubvrs  31457  altxpsspw  32084  matunitlindflem1  33405  poimirlem3  33412  poimirlem31  33440  poimirlem32  33441  mbfresfi  33456  itg2addnclem2  33462  ftc1anclem7  33491  ftc1anc  33493  hdmaplem2N  37061  hdmaplem3  37062  sucidVD  39108  mccllem  39829  limcresiooub  39874  limcresioolb  39875  cnrefiisplem  40055  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem1  40161  dvnprodlem2  40162  fourierdlem20  40344  fourierdlem38  40362  fourierdlem48  40371  fourierdlem49  40372  fourierdlem51  40374  fourierdlem62  40385  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem71  40394  fouriersw  40448  nnfoctbdjlem  40672  isomenndlem  40744  hoiprodp1  40802  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hspmbllem2  40841  pimrecltpos  40919  setsidel  41346