Theorem elun2 4149

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∪ cun 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  resf1extb  7913  dftpos4  8227  tfrlem11  8359  dif1en  9130  dif1enOLD  9132  findcard2d  9136  cantnfp1lem1  9638  cantnfp1lem3  9640  tc2  9702  rankunb  9810  rankelun  9832  djurcl  9871  djuss  9880  djuun  9886  dfac2b  10091  cfsmolem  10230  isfin4p1  10275  zornn0g  10465  mnfxr  11238  supxrun  13283  fsumsplitsnun  15728  sumsplit  15741  modfsummodslem1  15765  prmreclem5  16898  acsfiindd  18519  lspsolv  21060  mplcoe1  21951  maducoeval2  22534  restntr  23076  1stckgenlem  23447  fbun  23734  filuni  23779  ufileu  23813  alexsubALTlem4  23944  tmdgsum  23989  icccmplem2  24719  aannenlem2  26244  aalioulem2  26248  noetainflem4  27659  cutlt  27847  addsval  27876  addsrid  27878  addscom  27880  addsproplem4  27886  addsproplem5  27887  addsproplem6  27888  sleadd1  27903  addsass  27919  negsid  27954  mulsval  28019  mulsrid  28023  mulsproplem12  28037  mulscom  28049  addsdi  28065  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  onscutlt  28172  ebtwntg  28916  elntg  28918  elrspunsn  33407  bnj553  34895  bnj966  34941  bnj1442  35046  srcmpltd  35077  mrsubrn  35507  elmrsubrn  35514  mvhf  35552  msubvrs  35554  altxpsspw  35972  weiunse  36463  exrecfnlem  37374  matunitlindflem1  37617  poimirlem3  37624  poimirlem31  37652  poimirlem32  37653  mbfresfi  37667  itg2addnclem2  37673  ftc1anclem7  37700  ftc1anc  37702  hdmaplem2N  41773  hdmaplem3  41774  sucidVD  44868  nregmodellem  45013  pimxrneun  45491  mccllem  45602  limcresiooub  45647  limcresioolb  45648  cnrefiisplem  45834  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem1  45951  dvnprodlem2  45952  fourierdlem20  46132  fourierdlem38  46150  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem62  46173  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem71  46182  fouriersw  46236  nnfoctbdjlem  46460  isomenndlem  46535  hoiprodp1  46593  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hspmbllem2  46632  pimrecltpos  46713  setsidel  47381