Theorem coex 7927

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450   ∘ ccom 5659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666

This theorem is used by:  domtr  9013  enfixsn  9084  wdomtr  9547  cfcoflem  10274  axcc3  10440  axdc4uzlem  14047  hashfacen  14519  cofu1st  17972  cofu2nd  17974  cofucl  17977  fucid  18063  sursubmefmnd  19005  injsubmefmnd  19006  smndex1mgm  19019  gsumzaddlem  20048  cnfldfun  21599  cnfldfunALT  21600  znle  21749  selvval  22336  evls1fval  22544  evls1val  22545  evl1fval  22553  evl1val  22554  xkococnlem  23885  xkococn  23886  efmndtmd  24327  pserulm  26658  imsval  31166  tocycf  33557  eulerpartgbij  34883  derangenlem  35750  subfacp1lem5  35763  poimirlem9  38378  poimirlem15  38384  poimirlem17  38386  poimirlem20  38389  mbfresfi  38415  tendopl2  41650  erngplus2  41677  erngplus2-rN  41685  dvaplusgv  41883  dvhvaddass  41970  dvhlveclem  41981  diblss  42043  diblsmopel  42044  dicvaddcl  42063  dicvscacl  42064  cdlemn7  42076  dihordlem7  42087  dihopelvalcpre  42121  xihopellsmN  42127  dihopellsm  42128  rabren3dioph  43656  fzisoeu  46133  stirlinglem14  46915  fundcmpsurinjpreimafv  48308  grimco  48805  gricushgr  48833  cycldlenngric  48844  uspgrlim  48908  grlictr  48931  fuco22natlem  50271