Theorem elun2 4193

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  dftpos4  8269  wfrlem14OLD  8361  tfrlem11  8427  dif1en  9199  dif1enOLD  9201  findcard2d  9205  cantnfp1lem1  9716  cantnfp1lem3  9718  tc2  9780  rankunb  9888  rankelun  9910  djurcl  9949  djuss  9958  djuun  9964  dfac2b  10169  cfsmolem  10308  isfin4p1  10353  zornn0g  10543  mnfxr  11316  supxrun  13355  fsumsplitsnun  15788  sumsplit  15801  modfsummodslem1  15825  prmreclem5  16954  acsfiindd  18611  lspsolv  21163  mplcoe1  22073  maducoeval2  22662  restntr  23206  1stckgenlem  23577  fbun  23864  filuni  23909  ufileu  23943  alexsubALTlem4  24074  tmdgsum  24119  icccmplem2  24859  aannenlem2  26386  aalioulem2  26390  noetainflem4  27800  cutlt  27981  addsval  28010  addsrid  28012  addscom  28014  addsproplem4  28020  addsproplem5  28021  addsproplem6  28022  sleadd1  28037  addsass  28053  negsid  28088  mulsval  28150  mulsrid  28154  mulsproplem12  28168  mulscom  28180  addsdi  28196  precsexlem8  28253  precsexlem9  28254  precsexlem11  28256  ebtwntg  29012  elntg  29014  elrspunsn  33437  bnj553  34891  bnj966  34937  bnj1442  35042  srcmpltd  35073  mrsubrn  35498  elmrsubrn  35505  mvhf  35543  msubvrs  35545  altxpsspw  35959  weiunse  36451  exrecfnlem  37362  matunitlindflem1  37603  poimirlem3  37610  poimirlem31  37638  poimirlem32  37639  mbfresfi  37653  itg2addnclem2  37659  ftc1anclem7  37686  ftc1anc  37688  hdmaplem2N  41755  hdmaplem3  41756  metakunt22  42208  sucidVD  44870  pimxrneun  45439  mccllem  45553  limcresiooub  45598  limcresioolb  45599  cnrefiisplem  45785  dvmptfprodlem  45900  dvmptfprod  45901  dvnprodlem1  45902  dvnprodlem2  45903  fourierdlem20  46083  fourierdlem38  46101  fourierdlem48  46110  fourierdlem49  46111  fourierdlem51  46113  fourierdlem62  46124  fourierdlem63  46125  fourierdlem64  46126  fourierdlem65  46127  fourierdlem71  46133  fouriersw  46187  nnfoctbdjlem  46411  isomenndlem  46486  hoiprodp1  46544  hoidmvlelem1  46551  hoidmvlelem2  46552  hoidmvlelem3  46553  hoidmvlelem4  46554  hspmbllem2  46583  pimrecltpos  46664  setsidel  47301