Theorem elun1 4183

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  resf1extb  7980  brtpos  8290  dftpos4  8300  domunsncan  9134  unxpdomlem2  9286  rankunb  9901  rankelun  9926  djulcl  10028  djuss  10038  djuun  10044  fin1a2lem10  10526  zornn0g  10622  xrsupexmnf  13475  xrinfmexpnf  13476  sumsplit  15978  lcmfunsnlem2lem1  16857  lcmfunsnlem2  16859  prmreclem5  17142  smndex1mnd  19159  smndex1id  19160  gsumle  20410  lbsextlem3  21489  matunitlindflem1  23049  restntr  23555  comppfsc  23906  1stckgenlem  23927  fbun  24214  filconn  24257  filuni  24259  alexsubALTlem4  24424  ovolfiniun  25877  volfiniun  25923  elplyd  26575  ply1term  26577  aannenlem2  26713  aalioulem2  26717  eqcuts3  28247  cutlt  28375  addsval  28405  addsrid  28407  addscom  28409  addsproplem2  28413  addsproplem6  28417  leadds1  28432  addsass  28448  negsproplem2  28472  negsproplem6  28476  negsid  28484  mulsval  28552  mulsrid  28556  mulsproplem2  28560  mulsproplem3  28561  mulsproplem4  28562  mulsproplem5  28563  mulsproplem6  28564  mulsproplem7  28565  mulsproplem8  28566  mulsproplem12  28570  mulscom  28582  addsdi  28598  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  eengbas  29616  ecgrtg  29618  reprsuc  35355  bnj1498  35802  mrsubcn  36492  mrsubco  36494  altxpsspw  36957  weiunse  37471  poimirlem9  38815  poimirlem22  38828  poimirlem31  38837  poimirlem32  38838  mbfresfi  38852  itg2addnclem2  38858  ftc1anclem7  38885  ftc1anc  38887  hdmaplem1  43094  hdmap1eulem  43145  sucidALTVD  46112  sucidALT  46113  founiiun0  46478  pimxrneun  46771  mccllem  46882  limcresiooub  46925  limcresioolb  46926  cnrefiisplem  47112  dvmptfprodlem  47227  dvnprodlem2  47230  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem54  47443  fourierdlem62  47451  fourierdlem71  47460  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  fouriersw  47514  nnfoctbdjlem  47738  hoidmvlelem2  47879  hoidmvlelem3  47880  pimrecltpos  47991  setsnidel  48732