Theorem elun1 4148

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

Syntax hints:   → wi 4   ∈ wcel 2109   ∪ cun 3915

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  resf1extb  7913  brtpos  8217  dftpos4  8227  domunsncan  9046  unxpdomlem2  9205  rankunb  9810  rankelun  9832  djulcl  9870  djuss  9880  djuun  9886  fin1a2lem10  10369  zornn0g  10465  xrsupexmnf  13272  xrinfmexpnf  13273  sumsplit  15741  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  prmreclem5  16898  smndex1mnd  18844  smndex1id  18845  lbsextlem3  21077  restntr  23076  comppfsc  23426  1stckgenlem  23447  fbun  23734  filconn  23777  filuni  23779  alexsubALTlem4  23944  ovolfiniun  25409  volfiniun  25455  elplyd  26114  ply1term  26116  aannenlem2  26244  aalioulem2  26248  cutlt  27847  addsval  27876  addsrid  27878  addscom  27880  addsproplem2  27884  addsproplem6  27888  sleadd1  27903  addsass  27919  negsproplem2  27942  negsproplem6  27946  negsid  27954  mulsval  28019  mulsrid  28023  mulsproplem2  28027  mulsproplem3  28028  mulsproplem4  28029  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  mulsproplem12  28037  mulscom  28049  addsdi  28065  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  eengbas  28915  ecgrtg  28917  gsumle  33045  reprsuc  34613  bnj1498  35058  mrsubcn  35513  mrsubco  35515  altxpsspw  35972  weiunse  36463  matunitlindflem1  37617  poimirlem9  37630  poimirlem22  37643  poimirlem31  37652  poimirlem32  37653  mbfresfi  37667  itg2addnclem2  37673  ftc1anclem7  37700  ftc1anc  37702  hdmaplem1  41772  hdmap1eulem  41823  sucidALTVD  44866  sucidALT  44867  founiiun0  45191  pimxrneun  45491  mccllem  45602  limcresiooub  45647  limcresioolb  45648  cnrefiisplem  45834  dvmptfprodlem  45949  dvnprodlem2  45952  fourierdlem48  46159  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem62  46173  fourierdlem71  46182  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  fouriersw  46236  nnfoctbdjlem  46460  hoidmvlelem2  46601  hoidmvlelem3  46602  pimrecltpos  46713  setsnidel  47382