MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coex Structured version   Unicode version

Theorem coex 6541
Description: The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)
Hypotheses
Ref Expression
coex.1  |-  A  e. 
_V
coex.2  |-  B  e. 
_V
Assertion
Ref Expression
coex  |-  ( A  o.  B )  e. 
_V

Proof of Theorem coex
StepHypRef Expression
1 coex.1 . 2  |-  A  e. 
_V
2 coex.2 . 2  |-  B  e. 
_V
3 coexg 6540 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  o.  B
)  e.  _V )
41, 2, 3mp2an 672 1  |-  ( A  o.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2984    o. ccom 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-opab 4363  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863
This theorem is referenced by:  domtr  7374  enfixsn  7432  wdomtr  7802  cfcoflem  8453  axcc3  8619  axdc4uzlem  11816  hashfacen  12219  cofu1st  14805  cofu2nd  14807  cofucl  14810  fucid  14893  symgplusg  15906  gsumzaddlem  16420  evls1fval  17766  evls1val  17767  evl1fval  17774  evl1val  17775  znle  17979  xkococnlem  19244  xkococn  19245  symgtgp  19684  pserulm  21899  imsval  24088  eulerpartgbij  26767  derangenlem  27071  subfacp1lem5  27084  mbfresfi  28450  rabren3dioph  29166  stirlinglem14  29894  tendopl2  34433  erngplus2  34460  erngplus2-rN  34468  dvaplusgv  34666  dvhvaddass  34754  dvhlveclem  34765  diblss  34827  diblsmopel  34828  dicvaddcl  34847  dicvscacl  34848  cdlemn7  34860  dihordlem7  34871  dihopelvalcpre  34905  xihopellsmN  34911  dihopellsm  34912
  Copyright terms: Public domain W3C validator