Theorem elun2 3743

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

Syntax hints:   → wi 4   ∈ wcel 1977   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  dftpos4  7258  wfrlem14  7315  tfrlem11  7371  findcard2d  8087  cantnfp1lem1  8458  cantnfp1lem3  8460  tc2  8501  rankunb  8596  rankelun  8618  dfac2  8836  cfsmolem  8975  isfin4-3  9020  zornn0g  9210  mnfxr  9975  supxrun  12018  fsumsplitsnun  14328  sumsplit  14341  modfsummodslem1  14365  prmreclem5  15462  acsfiindd  17000  lspsolv  18964  mplcoe1  19286  maducoeval2  20265  restntr  20796  1stckgenlem  21166  fbun  21454  filuni  21499  ufileu  21533  alexsubALTlem4  21664  tmdgsum  21709  icccmplem2  22434  aannenlem2  23888  aalioulem2  23892  ebtwntg  25662  elntg  25664  bnj553  30222  bnj966  30268  bnj1442  30371  mrsubrn  30664  elmrsubrn  30671  mvhf  30709  msubvrs  30711  altxpsspw  31254  matunitlindflem1  32575  poimirlem3  32582  poimirlem31  32610  poimirlem32  32611  mbfresfi  32626  itg2addnclem2  32632  ftc1anclem7  32661  ftc1anc  32663  hdmaplem2N  36079  hdmaplem3  36080  sucidVD  38130  mccllem  38664  limcresiooub  38709  limcresioolb  38710  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem1  38836  dvnprodlem2  38837  fourierdlem20  39020  fourierdlem38  39038  fourierdlem48  39047  fourierdlem49  39048  fourierdlem51  39050  fourierdlem62  39061  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem71  39070  fouriersw  39124  nnfoctbdjlem  39348  isomenndlem  39420  hoiprodp1  39478  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hspmbllem2  39517  pimrecltpos  39596