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

Theorem coex 5376
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 5375 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  o.  B
)  e.  _V )
41, 2, 3mp2an 654 1  |-  ( A  o.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2920    o. ccom 4845
This theorem is referenced by:  domtr  7123  wdomtr  7503  cfcoflem  8112  axcc3  8278  axdc4uzlem  11280  hashfacen  11662  cofu1st  14039  cofu2nd  14041  cofucl  14044  fucid  14127  symgplusg  15058  znle  16776  xkococnlem  17648  xkococn  17649  symgtgp  18088  evl1fval  19904  evl1val  19905  pserulm  20295  imsval  22134  derangenlem  24814  subfacp1lem5  24827  mbfresfi  26156  rabren3dioph  26770  enfixsn  27129  stirlinglem14  27707  tendopl2  31263  erngplus2  31290  erngplus2-rN  31298  dvaplusgv  31496  dvhvaddass  31584  dvhlveclem  31595  diblss  31657  diblsmopel  31658  dicvaddcl  31677  dicvscacl  31678  cdlemn7  31690  dihordlem7  31701  dihopelvalcpre  31735  xihopellsmN  31741  dihopellsm  31742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852
  Copyright terms: Public domain W3C validator