Theorem elun1 4131

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∪ cun 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  resf1extb  7935  brtpos  8237  dftpos4  8247  domunsncan  9079  unxpdomlem2  9231  rankunb  9836  rankelun  9858  djulcl  9919  djuss  9929  djuun  9935  fin1a2lem10  10415  zornn0g  10511  xrsupexmnf  13361  xrinfmexpnf  13362  sumsplit  15858  lcmfunsnlem2lem1  16734  lcmfunsnlem2  16736  prmreclem5  17018  smndex1mnd  19028  smndex1id  19029  gsumle  20278  lbsextlem3  21353  matunitlindflem1  22907  restntr  23413  comppfsc  23764  1stckgenlem  23785  fbun  24072  filconn  24115  filuni  24117  alexsubALTlem4  24282  ovolfiniun  25735  volfiniun  25781  elplyd  26434  ply1term  26436  aannenlem2  26572  aalioulem2  26576  eqcuts3  28077  cutlt  28205  addsval  28235  addsrid  28237  addscom  28239  addsproplem2  28243  addsproplem6  28247  leadds1  28262  addsass  28278  negsproplem2  28302  negsproplem6  28306  negsid  28314  mulsval  28382  mulsrid  28386  mulsproplem2  28390  mulsproplem3  28391  mulsproplem4  28392  mulsproplem5  28393  mulsproplem6  28394  mulsproplem7  28395  mulsproplem8  28396  mulsproplem12  28400  mulscom  28412  addsdi  28428  precsexlem8  28487  precsexlem9  28488  precsexlem11  28490  eengbas  29446  ecgrtg  29448  reprsuc  35131  bnj1498  35578  mrsubcn  36106  mrsubco  36108  altxpsspw  36565  weiunse  37095  poimirlem9  38386  poimirlem22  38399  poimirlem31  38408  poimirlem32  38409  mbfresfi  38423  itg2addnclem2  38429  ftc1anclem7  38456  ftc1anc  38458  hdmaplem1  42652  hdmap1eulem  42703  sucidALTVD  45700  sucidALT  45701  founiiun0  46030  pimxrneun  46324  mccllem  46435  limcresiooub  46478  limcresioolb  46479  cnrefiisplem  46665  dvmptfprodlem  46780  dvnprodlem2  46783  fourierdlem48  46990  fourierdlem49  46991  fourierdlem51  46993  fourierdlem54  46996  fourierdlem62  47004  fourierdlem71  47013  fourierdlem103  47045  fourierdlem104  47046  fourierdlem114  47056  fouriersw  47067  nnfoctbdjlem  47291  hoidmvlelem2  47432  hoidmvlelem3  47433  pimrecltpos  47544  setsnidel  48285