Theorem elun2 4129

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  srcmpltd  4432  resf1extb  7944  dftpos4  8255  tfrlem11  8389  dif1en  9170  findcard2d  9175  cantnfp1lem1  9672  cantnfp1lem3  9674  tc2  9734  rankunb  9857  rankelun  9882  djurcl  9985  djuss  9994  djuun  10000  dfac2b  10202  cfsmolem  10341  isfin4p1  10386  zornn0g  10576  mnfxr  11359  supxrun  13439  fsumsplitsnun  15914  sumsplit  15927  modfsummodslem1  15952  prmreclem5  17091  acsfiindd  18720  lspsolv  21414  mplcoe1  22339  maducoeval2  22948  matunitlindflem1  22987  restntr  23493  1stckgenlem  23865  fbun  24152  filuni  24197  ufileu  24231  alexsubALTlem4  24362  tmdgsum  24407  icccmplem2  25136  aannenlem2  26649  aalioulem2  26653  noetainflem4  28090  eqcuts3  28183  cutlt  28311  addsval  28341  addsrid  28343  addscom  28345  addsproplem4  28351  addsproplem5  28352  addsproplem6  28353  leadds1  28368  addsass  28384  negsid  28420  mulsval  28488  mulsrid  28492  mulsproplem12  28506  mulscom  28518  addsdi  28534  precsexlem8  28593  precsexlem9  28594  precsexlem11  28596  oncutlt  28643  ebtwntg  29553  elntg  29555  elrspunsn  33972  mplidomlem  34152  bnj553  35521  bnj966  35567  bnj1442  35672  mrsubrn  36257  elmrsubrn  36264  mvhf  36302  msubvrs  36304  altxpsspw  36722  weiunse  37236  exrecfnlem  38282  poimirlem3  38521  poimirlem31  38549  poimirlem32  38550  mbfresfi  38564  itg2addnclem2  38570  ftc1anclem7  38597  ftc1anc  38599  hdmaplem2N  42809  hdmaplem3  42810  sucidVD  45839  nregmodellem  45984  pimxrneun  46467  mccllem  46578  limcresiooub  46621  limcresioolb  46622  cnrefiisplem  46808  dvmptfprodlem  46923  dvmptfprod  46924  dvnprodlem1  46925  dvnprodlem2  46926  fourierdlem20  47106  fourierdlem38  47124  fourierdlem48  47133  fourierdlem49  47134  fourierdlem51  47136  fourierdlem62  47147  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem71  47156  fouriersw  47210  nnfoctbdjlem  47434  isomenndlem  47509  hoiprodp1  47567  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoidmvlelem4  47577  hspmbllem2  47606  pimrecltpos  47687  setsidel  48427