Theorem coex 7924

Description: The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)

Hypotheses

Ref	Expression
coex.1	⊢ 𝐴 ∈ V
coex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
coex	⊢ (𝐴 ∘ 𝐵) ∈ V

Proof of Theorem coex

Step	Hyp	Ref	Expression
1		coex.1	. 2 ⊢ 𝐴 ∈ V
2		coex.2	. 2 ⊢ 𝐵 ∈ V
3		coexg 7923	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∘ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∘ ccom 5658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665

This theorem is referenced by:  domtr  9019  enfixsn  9093  wdomtr  9587  cfcoflem  10284  axcc3  10450  axdc4uzlem  13999  hashfacen  14470  cofu1st  17894  cofu2nd  17896  cofucl  17899  fucid  17985  sursubmefmnd  18872  injsubmefmnd  18873  smndex1mgm  18883  gsumzaddlem  19900  cnfldfun  21327  cnfldfunALT  21328  cnfldfunOLD  21340  cnfldfunALTOLD  21341  znle  21495  selvval  22071  evls1fval  22255  evls1val  22256  evl1fval  22264  evl1val  22265  xkococnlem  23595  xkococn  23596  efmndtmd  24037  pserulm  26381  imsval  30612  tocycf  33074  eulerpartgbij  34350  derangenlem  35139  subfacp1lem5  35152  poimirlem9  37599  poimirlem15  37605  poimirlem17  37607  poimirlem20  37610  mbfresfi  37636  tendopl2  40742  erngplus2  40769  erngplus2-rN  40777  dvaplusgv  40975  dvhvaddass  41062  dvhlveclem  41073  diblss  41135  diblsmopel  41136  dicvaddcl  41155  dicvscacl  41156  cdlemn7  41168  dihordlem7  41179  dihopelvalcpre  41213  xihopellsmN  41219  dihopellsm  41220  rabren3dioph  42785  fzisoeu  45277  stirlinglem14  46064  fundcmpsurinjpreimafv  47370  grimco  47850  gricushgr  47878  cycldlenngric  47889  uspgrlim  47952  grlictr  47968  fuco22natlem  49204