Theorem elun2 4183

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  resf1extb  7956  dftpos4  8270  wfrlem14OLD  8362  tfrlem11  8428  dif1en  9200  dif1enOLD  9202  findcard2d  9206  cantnfp1lem1  9718  cantnfp1lem3  9720  tc2  9782  rankunb  9890  rankelun  9912  djurcl  9951  djuss  9960  djuun  9966  dfac2b  10171  cfsmolem  10310  isfin4p1  10355  zornn0g  10545  mnfxr  11318  supxrun  13358  fsumsplitsnun  15791  sumsplit  15804  modfsummodslem1  15828  prmreclem5  16958  acsfiindd  18598  lspsolv  21145  mplcoe1  22055  maducoeval2  22646  restntr  23190  1stckgenlem  23561  fbun  23848  filuni  23893  ufileu  23927  alexsubALTlem4  24058  tmdgsum  24103  icccmplem2  24845  aannenlem2  26371  aalioulem2  26375  noetainflem4  27785  cutlt  27966  addsval  27995  addsrid  27997  addscom  27999  addsproplem4  28005  addsproplem5  28006  addsproplem6  28007  sleadd1  28022  addsass  28038  negsid  28073  mulsval  28135  mulsrid  28139  mulsproplem12  28153  mulscom  28165  addsdi  28181  precsexlem8  28238  precsexlem9  28239  precsexlem11  28241  ebtwntg  28997  elntg  28999  elrspunsn  33457  bnj553  34912  bnj966  34958  bnj1442  35063  srcmpltd  35094  mrsubrn  35518  elmrsubrn  35525  mvhf  35563  msubvrs  35565  altxpsspw  35978  weiunse  36469  exrecfnlem  37380  matunitlindflem1  37623  poimirlem3  37630  poimirlem31  37658  poimirlem32  37659  mbfresfi  37673  itg2addnclem2  37679  ftc1anclem7  37706  ftc1anc  37708  hdmaplem2N  41774  hdmaplem3  41775  metakunt22  42227  sucidVD  44892  pimxrneun  45499  mccllem  45612  limcresiooub  45657  limcresioolb  45658  cnrefiisplem  45844  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem1  45961  dvnprodlem2  45962  fourierdlem20  46142  fourierdlem38  46160  fourierdlem48  46169  fourierdlem49  46170  fourierdlem51  46172  fourierdlem62  46183  fourierdlem63  46184  fourierdlem64  46185  fourierdlem65  46186  fourierdlem71  46192  fouriersw  46246  nnfoctbdjlem  46470  isomenndlem  46545  hoiprodp1  46603  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hspmbllem2  46642  pimrecltpos  46723  setsidel  47363