Theorem elun2 4158

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∪ cun 3924

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943

This theorem is referenced by:  resf1extb  7930  dftpos4  8244  wfrlem14OLD  8336  tfrlem11  8402  dif1en  9174  dif1enOLD  9176  findcard2d  9180  cantnfp1lem1  9692  cantnfp1lem3  9694  tc2  9756  rankunb  9864  rankelun  9886  djurcl  9925  djuss  9934  djuun  9940  dfac2b  10145  cfsmolem  10284  isfin4p1  10329  zornn0g  10519  mnfxr  11292  supxrun  13332  fsumsplitsnun  15771  sumsplit  15784  modfsummodslem1  15808  prmreclem5  16940  acsfiindd  18563  lspsolv  21104  mplcoe1  21995  maducoeval2  22578  restntr  23120  1stckgenlem  23491  fbun  23778  filuni  23823  ufileu  23857  alexsubALTlem4  23988  tmdgsum  24033  icccmplem2  24763  aannenlem2  26289  aalioulem2  26293  noetainflem4  27704  cutlt  27892  addsval  27921  addsrid  27923  addscom  27925  addsproplem4  27931  addsproplem5  27932  addsproplem6  27933  sleadd1  27948  addsass  27964  negsid  27999  mulsval  28064  mulsrid  28068  mulsproplem12  28082  mulscom  28094  addsdi  28110  precsexlem8  28168  precsexlem9  28169  precsexlem11  28171  onscutlt  28217  ebtwntg  28961  elntg  28963  elrspunsn  33444  bnj553  34929  bnj966  34975  bnj1442  35080  srcmpltd  35111  mrsubrn  35535  elmrsubrn  35542  mvhf  35580  msubvrs  35582  altxpsspw  35995  weiunse  36486  exrecfnlem  37397  matunitlindflem1  37640  poimirlem3  37647  poimirlem31  37675  poimirlem32  37676  mbfresfi  37690  itg2addnclem2  37696  ftc1anclem7  37723  ftc1anc  37725  hdmaplem2N  41791  hdmaplem3  41792  metakunt22  42239  sucidVD  44896  pimxrneun  45515  mccllem  45626  limcresiooub  45671  limcresioolb  45672  cnrefiisplem  45858  dvmptfprodlem  45973  dvmptfprod  45974  dvnprodlem1  45975  dvnprodlem2  45976  fourierdlem20  46156  fourierdlem38  46174  fourierdlem48  46183  fourierdlem49  46184  fourierdlem51  46186  fourierdlem62  46197  fourierdlem63  46198  fourierdlem64  46199  fourierdlem65  46200  fourierdlem71  46206  fouriersw  46260  nnfoctbdjlem  46484  isomenndlem  46559  hoiprodp1  46617  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  hspmbllem2  46656  pimrecltpos  46737  setsidel  47390