Theorem elun2 4155

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954

This theorem is referenced by:  dftpos4  7913  wfrlem14  7970  tfrlem11  8026  findcard2d  8762  cantnfp1lem1  9143  cantnfp1lem3  9145  tc2  9186  rankunb  9281  rankelun  9303  djurcl  9342  djuss  9351  djuun  9357  dfac2b  9558  cfsmolem  9694  isfin4p1  9739  zornn0g  9929  mnfxr  10700  supxrun  12712  fsumsplitsnun  15112  sumsplit  15125  modfsummodslem1  15149  prmreclem5  16258  acsfiindd  17789  lspsolv  19917  mplcoe1  20248  maducoeval2  21251  restntr  21792  1stckgenlem  22163  fbun  22450  filuni  22495  ufileu  22529  alexsubALTlem4  22660  tmdgsum  22705  icccmplem2  23433  aannenlem2  24920  aalioulem2  24924  ebtwntg  26770  elntg  26772  bnj553  32172  bnj966  32218  bnj1442  32323  srcmpltd  32348  mrsubrn  32762  elmrsubrn  32769  mvhf  32807  msubvrs  32809  altxpsspw  33440  exrecfnlem  34662  matunitlindflem1  34890  poimirlem3  34897  poimirlem31  34925  poimirlem32  34926  mbfresfi  34940  itg2addnclem2  34946  ftc1anclem7  34975  ftc1anc  34977  hdmaplem2N  38910  hdmaplem3  38911  sucidVD  41213  mccllem  41885  limcresiooub  41930  limcresioolb  41931  cnrefiisplem  42117  dvmptfprodlem  42236  dvmptfprod  42237  dvnprodlem1  42238  dvnprodlem2  42239  fourierdlem20  42419  fourierdlem38  42437  fourierdlem48  42446  fourierdlem49  42447  fourierdlem51  42449  fourierdlem62  42460  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  fourierdlem71  42469  fouriersw  42523  nnfoctbdjlem  42744  isomenndlem  42819  hoiprodp1  42877  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem3  42886  hoidmvlelem4  42887  hspmbllem2  42916  pimrecltpos  42994  setsidel  43543