Theorem coex 7943

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 7942	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
4	1, 2, 3	mp2an 705	1 ⊢ (𝐴 ∘ 𝐵) ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661

This theorem is used by:  domtr  9038  enfixsn  9109  wdomtr  9573  cfcoflem  10354  axcc3  10520  axdc4uzlem  14130  hashfacen  14603  cofu1st  18064  cofu2nd  18066  cofucl  18069  fucid  18155  sursubmefmnd  19098  injsubmefmnd  19099  smndex1mgm  19112  gsumzaddlem  20141  cnfldfun  21698  cnfldfunALT  21699  znle  21848  selvval  22435  evls1fval  22643  evls1val  22644  evl1fval  22652  evl1val  22653  xkococnlem  23984  xkococn  23985  efmndtmd  24426  pserulm  26755  imsval  31293  tocycf  33725  eulerpartgbij  35051  derangenlem  36023  subfacp1lem5  36036  poimirlem9  38641  poimirlem15  38647  poimirlem17  38649  poimirlem20  38652  mbfresfi  38678  tendopl2  41928  erngplus2  41955  erngplus2-rN  41963  dvaplusgv  42161  dvhvaddass  42248  dvhlveclem  42259  diblss  42321  diblsmopel  42322  dicvaddcl  42341  dicvscacl  42342  cdlemn7  42354  dihordlem7  42365  dihopelvalcpre  42399  xihopellsmN  42405  dihopellsm  42406  rabren3dioph  43916  fzisoeu  46410  stirlinglem14  47191  fundcmpsurinjpreimafv  48584  grimco  49081  gricushgr  49109  cycldlenngric  49120  uspgrlim  49184  grlictr  49207  fuco22natlem  50561