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

Theorem coex 5448
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 5447 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( A  o.  B
)  e.  _V )
41, 2, 3mp2an 655 1  |-  ( A  o.  B )  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1728   _Vcvv 2965    o. ccom 4917
This theorem is referenced by:  domtr  7196  wdomtr  7579  cfcoflem  8190  axcc3  8356  axdc4uzlem  11359  hashfacen  11741  cofu1st  14118  cofu2nd  14120  cofucl  14123  fucid  14206  symgplusg  15137  znle  16855  xkococnlem  17729  xkococn  17730  symgtgp  18169  evl1fval  19985  evl1val  19986  pserulm  20376  imsval  22215  derangenlem  24892  subfacp1lem5  24905  mbfresfi  26293  rabren3dioph  26988  enfixsn  27346  stirlinglem14  27924  tendopl2  31748  erngplus2  31775  erngplus2-rN  31783  dvaplusgv  31981  dvhvaddass  32069  dvhlveclem  32080  diblss  32142  diblsmopel  32143  dicvaddcl  32162  dicvscacl  32163  cdlemn7  32175  dihordlem7  32186  dihopelvalcpre  32220  xihopellsmN  32226  dihopellsm  32227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924
  Copyright terms: Public domain W3C validator