Theorem elun2 4038

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

Syntax hints:   → wi 4   ∈ wcel 2048   ∪ cun 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-un 3830  df-in 3832  df-ss 3839

This theorem is referenced by:  dftpos4  7707  wfrlem14  7765  tfrlem11  7821  findcard2d  8547  cantnfp1lem1  8927  cantnfp1lem3  8929  tc2  8970  rankunb  9065  rankelun  9087  djurcl  9126  djuss  9135  djuun  9141  dfac2b  9342  cfsmolem  9482  isfin4p1  9527  zornn0g  9717  mnfxr  10490  supxrun  12518  fsumsplitsnun  14960  sumsplit  14973  modfsummodslem1  14997  prmreclem5  16102  acsfiindd  17635  lspsolv  19627  mplcoe1  19949  maducoeval2  20943  restntr  21484  1stckgenlem  21855  fbun  22142  filuni  22187  ufileu  22221  alexsubALTlem4  22352  tmdgsum  22397  icccmplem2  23124  aannenlem2  24611  aalioulem2  24615  ebtwntg  26461  elntg  26463  bnj553  31778  bnj966  31824  bnj1442  31927  mrsubrn  32220  elmrsubrn  32227  mvhf  32265  msubvrs  32267  altxpsspw  32899  exrecfnlem  34037  matunitlindflem1  34277  poimirlem3  34284  poimirlem31  34312  poimirlem32  34313  mbfresfi  34327  itg2addnclem2  34333  ftc1anclem7  34362  ftc1anc  34364  hdmaplem2N  38301  hdmaplem3  38302  sucidVD  40569  mccllem  41255  limcresiooub  41300  limcresioolb  41301  cnrefiisplem  41487  dvmptfprodlem  41605  dvmptfprod  41606  dvnprodlem1  41607  dvnprodlem2  41608  fourierdlem20  41789  fourierdlem38  41807  fourierdlem48  41816  fourierdlem49  41817  fourierdlem51  41819  fourierdlem62  41830  fourierdlem63  41831  fourierdlem64  41832  fourierdlem65  41833  fourierdlem71  41839  fouriersw  41893  nnfoctbdjlem  42114  isomenndlem  42189  hoiprodp1  42247  hoidmvlelem1  42254  hoidmvlelem2  42255  hoidmvlelem3  42256  hoidmvlelem4  42257  hspmbllem2  42286  pimrecltpos  42364  setsidel  42888