Theorem elun1 4141

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  resf1extb  7890  brtpos  8191  dftpos4  8201  domunsncan  9018  unxpdomlem2  9174  rankunb  9779  rankelun  9801  djulcl  9839  djuss  9849  djuun  9855  fin1a2lem10  10338  zornn0g  10434  xrsupexmnf  13241  xrinfmexpnf  13242  sumsplit  15710  lcmfunsnlem2lem1  16584  lcmfunsnlem2  16586  prmreclem5  16867  smndex1mnd  18819  smndex1id  18820  gsumle  20059  lbsextlem3  21102  restntr  23102  comppfsc  23452  1stckgenlem  23473  fbun  23760  filconn  23803  filuni  23805  alexsubALTlem4  23970  ovolfiniun  25435  volfiniun  25481  elplyd  26140  ply1term  26142  aannenlem2  26270  aalioulem2  26274  eqscut3  27770  cutlt  27880  addsval  27909  addsrid  27911  addscom  27913  addsproplem2  27917  addsproplem6  27921  sleadd1  27936  addsass  27952  negsproplem2  27975  negsproplem6  27979  negsid  27987  mulsval  28052  mulsrid  28056  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  mulsproplem12  28070  mulscom  28082  addsdi  28098  precsexlem8  28156  precsexlem9  28157  precsexlem11  28159  eengbas  28961  ecgrtg  28963  reprsuc  34599  bnj1498  35044  mrsubcn  35499  mrsubco  35501  altxpsspw  35958  weiunse  36449  matunitlindflem1  37603  poimirlem9  37616  poimirlem22  37629  poimirlem31  37638  poimirlem32  37639  mbfresfi  37653  itg2addnclem2  37659  ftc1anclem7  37686  ftc1anc  37688  hdmaplem1  41758  hdmap1eulem  41809  sucidALTVD  44852  sucidALT  44853  founiiun0  45177  pimxrneun  45477  mccllem  45588  limcresiooub  45633  limcresioolb  45634  cnrefiisplem  45820  dvmptfprodlem  45935  dvnprodlem2  45938  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem54  46151  fourierdlem62  46159  fourierdlem71  46168  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  fouriersw  46222  nnfoctbdjlem  46446  hoidmvlelem2  46587  hoidmvlelem3  46588  pimrecltpos  46699  setsnidel  47371