Theorem elun1 4123

Description: Membership law for union of classes. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
elun1	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 4119	. 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
2	1	sseli 3918	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  resf1extb  7879  brtpos  8179  dftpos4  8189  domunsncan  9009  unxpdomlem2  9161  rankunb  9768  rankelun  9790  djulcl  9828  djuss  9838  djuun  9844  fin1a2lem10  10325  zornn0g  10421  xrsupexmnf  13251  xrinfmexpnf  13252  sumsplit  15724  lcmfunsnlem2lem1  16601  lcmfunsnlem2  16603  prmreclem5  16885  smndex1mnd  18875  smndex1id  18876  gsumle  20114  lbsextlem3  21153  restntr  23160  comppfsc  23510  1stckgenlem  23531  fbun  23818  filconn  23861  filuni  23863  alexsubALTlem4  24028  ovolfiniun  25481  volfiniun  25527  elplyd  26180  ply1term  26182  aannenlem2  26309  aalioulem2  26313  eqcuts3  27813  cutlt  27941  addsval  27971  addsrid  27973  addscom  27975  addsproplem2  27979  addsproplem6  27983  leadds1  27998  addsass  28014  negsproplem2  28038  negsproplem6  28042  negsid  28050  mulsval  28118  mulsrid  28122  mulsproplem2  28126  mulsproplem3  28127  mulsproplem4  28128  mulsproplem5  28129  mulsproplem6  28130  mulsproplem7  28131  mulsproplem8  28132  mulsproplem12  28136  mulscom  28148  addsdi  28164  precsexlem8  28223  precsexlem9  28224  precsexlem11  28226  eengbas  29067  ecgrtg  29069  reprsuc  34778  bnj1498  35222  mrsubcn  35720  mrsubco  35722  altxpsspw  36178  weiunse  36669  matunitlindflem1  37954  poimirlem9  37967  poimirlem22  37980  poimirlem31  37989  poimirlem32  37990  mbfresfi  38004  itg2addnclem2  38010  ftc1anclem7  38037  ftc1anc  38039  hdmaplem1  42234  hdmap1eulem  42285  sucidALTVD  45317  sucidALT  45318  founiiun0  45641  pimxrneun  45937  mccllem  46048  limcresiooub  46091  limcresioolb  46092  cnrefiisplem  46278  dvmptfprodlem  46393  dvnprodlem2  46396  fourierdlem48  46603  fourierdlem49  46604  fourierdlem51  46606  fourierdlem54  46609  fourierdlem62  46617  fourierdlem71  46626  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  fouriersw  46680  nnfoctbdjlem  46904  hoidmvlelem2  47045  hoidmvlelem3  47046  pimrecltpos  47157  setsnidel  47852