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

Theorem coex 6698
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 6697 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  o.  B
)  e.  _V )
41, 2, 3mp2an 676 1  |-  ( A  o.  B )  e. 
_V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   _Vcvv 3017    o. ccom 4795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-br 4362  df-opab 4421  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802
This theorem is referenced by:  domtr  7571  enfixsn  7629  wdomtr  8038  cfcoflem  8648  axcc3  8814  axdc4uzlem  12140  hashfacen  12560  cofu1st  15726  cofu2nd  15728  cofucl  15731  fucid  15814  symgplusg  16968  gsumzaddlem  17492  evls1fval  18846  evls1val  18847  evl1fval  18854  evl1val  18855  znle  19044  xkococnlem  20611  xkococn  20612  symgtgp  21053  pserulm  23314  imsval  26254  eulerpartgbij  29152  derangenlem  29841  subfacp1lem5  29854  poimirlem9  31856  poimirlem15  31862  poimirlem17  31864  poimirlem20  31867  mbfresfi  31894  tendopl2  34256  erngplus2  34283  erngplus2-rN  34291  dvaplusgv  34489  dvhvaddass  34577  dvhlveclem  34588  diblss  34650  diblsmopel  34651  dicvaddcl  34670  dicvscacl  34671  cdlemn7  34683  dihordlem7  34694  dihopelvalcpre  34728  xihopellsmN  34734  dihopellsm  34735  rabren3dioph  35570  fzisoeu  37415  stirlinglem14  37832
  Copyright terms: Public domain W3C validator