Theorem elun1 4135

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  resf1extb  7927  brtpos  8227  dftpos4  8237  domunsncan  9061  unxpdomlem2  9213  rankunb  9818  rankelun  9840  djulcl  9892  djuss  9902  djuun  9908  fin1a2lem10  10388  zornn0g  10484  xrsupexmnf  13326  xrinfmexpnf  13327  sumsplit  15815  lcmfunsnlem2lem1  16691  lcmfunsnlem2  16693  prmreclem5  16975  smndex1mnd  18967  smndex1id  18968  gsumle  20210  lbsextlem3  21284  restntr  23339  comppfsc  23689  1stckgenlem  23710  fbun  23997  filconn  24040  filuni  24042  alexsubALTlem4  24207  ovolfiniun  25660  volfiniun  25706  elplyd  26359  ply1term  26361  aannenlem2  26492  aalioulem2  26496  eqcuts3  27997  cutlt  28125  addsval  28155  addsrid  28157  addscom  28159  addsproplem2  28163  addsproplem6  28167  leadds1  28182  addsass  28198  negsproplem2  28222  negsproplem6  28226  negsid  28234  mulsval  28302  mulsrid  28306  mulsproplem2  28310  mulsproplem3  28311  mulsproplem4  28312  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  mulsproplem12  28320  mulscom  28332  addsdi  28348  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  eengbas  29331  ecgrtg  29333  reprsuc  35002  bnj1498  35449  mrsubcn  36011  mrsubco  36013  altxpsspw  36469  weiunse  36999  matunitlindflem1  38287  poimirlem9  38300  poimirlem22  38313  poimirlem31  38322  poimirlem32  38323  mbfresfi  38337  itg2addnclem2  38343  ftc1anclem7  38370  ftc1anc  38372  hdmaplem1  42565  hdmap1eulem  42616  sucidALTVD  45598  sucidALT  45599  founiiun0  45928  pimxrneun  46222  mccllem  46333  limcresiooub  46376  limcresioolb  46377  cnrefiisplem  46563  dvmptfprodlem  46678  dvnprodlem2  46681  fourierdlem48  46888  fourierdlem49  46889  fourierdlem51  46891  fourierdlem54  46894  fourierdlem62  46902  fourierdlem71  46911  fourierdlem103  46943  fourierdlem104  46944  fourierdlem114  46954  fouriersw  46965  nnfoctbdjlem  47189  hoidmvlelem2  47330  hoidmvlelem3  47331  pimrecltpos  47442  setsnidel  48146