Theorem elun2 4180

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150

This theorem is used by:  srcmpltd  4431  resf1extb  7950  dftpos4  8269  tfrlem11  8403  dif1en  9184  findcard2d  9189  cantnfp1lem1  9686  cantnfp1lem3  9688  tc2  9748  rankunb  9871  rankelun  9896  djurcl  9999  djuss  10008  djuun  10014  dfac2b  10216  cfsmolem  10355  isfin4p1  10400  zornn0g  10590  mnfxr  11373  supxrun  13453  fsumsplitsnun  15930  sumsplit  15943  modfsummodslem1  15968  prmreclem5  17107  acsfiindd  18736  lspsolv  21430  mplcoe1  22355  maducoeval2  22964  matunitlindflem1  23003  restntr  23509  1stckgenlem  23881  fbun  24168  filuni  24213  ufileu  24247  alexsubALTlem4  24378  tmdgsum  24423  icccmplem2  25152  aannenlem2  26665  aalioulem2  26669  noetainflem4  28106  eqcuts3  28199  cutlt  28327  addsval  28357  addsrid  28359  addscom  28361  addsproplem4  28367  addsproplem5  28368  addsproplem6  28369  leadds1  28384  addsass  28400  negsid  28436  mulsval  28504  mulsrid  28508  mulsproplem12  28522  mulscom  28534  addsdi  28550  precsexlem8  28609  precsexlem9  28610  precsexlem11  28612  oncutlt  28659  ebtwntg  29569  elntg  29571  elrspunsn  34029  mplidomlem  34209  bnj553  35578  bnj966  35624  bnj1442  35729  mrsubrn  36368  elmrsubrn  36375  mvhf  36413  msubvrs  36415  altxpsspw  36838  weiunse  37352  exrecfnlem  38411  poimirlem3  38650  poimirlem31  38678  poimirlem32  38679  mbfresfi  38693  itg2addnclem2  38699  ftc1anclem7  38726  ftc1anc  38728  hdmaplem2N  42938  hdmaplem3  42939  sucidVD  45962  nregmodellem  46114  pimxrneun  46606  mccllem  46717  limcresiooub  46760  limcresioolb  46761  cnrefiisplem  46947  dvmptfprodlem  47062  dvmptfprod  47063  dvnprodlem1  47064  dvnprodlem2  47065  fourierdlem20  47245  fourierdlem38  47263  fourierdlem48  47272  fourierdlem49  47273  fourierdlem51  47275  fourierdlem62  47286  fourierdlem63  47287  fourierdlem64  47288  fourierdlem65  47289  fourierdlem71  47295  fouriersw  47349  nnfoctbdjlem  47573  isomenndlem  47648  hoiprodp1  47706  hoidmvlelem1  47713  hoidmvlelem2  47714  hoidmvlelem3  47715  hoidmvlelem4  47716  hspmbllem2  47745  pimrecltpos  47826  setsidel  48566  parcatid2  50871  parcatid  50872