Theorem elun2 4184

Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
elun2	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Proof of Theorem elun2

Step	Hyp	Ref	Expression
1		ssun2 4180	. 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:  srcmpltd  4435  resf1extb  7980  dftpos4  8300  tfrlem11  8434  dif1en  9215  findcard2d  9220  cantnfp1lem1  9716  cantnfp1lem3  9718  tc2  9778  rankunb  9901  rankelun  9926  djurcl  10029  djuss  10038  djuun  10044  dfac2b  10248  cfsmolem  10387  isfin4p1  10432  zornn0g  10622  mnfxr  11405  supxrun  13486  fsumsplitsnun  15965  sumsplit  15978  modfsummodslem1  16003  prmreclem5  17142  acsfiindd  18777  lspsolv  21472  mplcoe1  22401  maducoeval2  23010  matunitlindflem1  23049  restntr  23555  1stckgenlem  23927  fbun  24214  filuni  24259  ufileu  24293  alexsubALTlem4  24424  tmdgsum  24469  icccmplem2  25198  aannenlem2  26713  aalioulem2  26717  noetainflem4  28154  eqcuts3  28247  cutlt  28375  addsval  28405  addsrid  28407  addscom  28409  addsproplem4  28415  addsproplem5  28416  addsproplem6  28417  leadds1  28432  addsass  28448  negsid  28484  mulsval  28552  mulsrid  28556  mulsproplem12  28570  mulscom  28582  addsdi  28598  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  oncutlt  28707  ebtwntg  29617  elntg  29619  elrspunsn  34083  mplidomlem  34270  bnj553  35639  bnj966  35685  bnj1442  35790  mrsubrn  36486  elmrsubrn  36493  mvhf  36531  msubvrs  36533  altxpsspw  36957  weiunse  37471  exrecfnlem  38570  poimirlem3  38809  poimirlem31  38837  poimirlem32  38838  mbfresfi  38852  itg2addnclem2  38858  ftc1anclem7  38885  ftc1anc  38887  hdmaplem2N  43095  hdmaplem3  43096  sucidVD  46114  nregmodellem  46270  pimxrneun  46771  mccllem  46882  limcresiooub  46925  limcresioolb  46926  cnrefiisplem  47112  dvmptfprodlem  47227  dvmptfprod  47228  dvnprodlem1  47229  dvnprodlem2  47230  fourierdlem20  47410  fourierdlem38  47428  fourierdlem48  47437  fourierdlem49  47438  fourierdlem51  47440  fourierdlem62  47451  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem71  47460  fouriersw  47514  nnfoctbdjlem  47738  isomenndlem  47813  hoiprodp1  47871  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  hspmbllem2  47910  pimrecltpos  47991  setsidel  48731  parcatid2  51094  parcatid  51095