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 2145  Vcvv 3451   ∘ ccom 5655

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 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7752

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3900  df-un 3902  df-in 3904  df-ss 3915  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 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662

This theorem is used by:  domtr  9035  enfixsn  9106  wdomtr  9570  cfcoflem  10351  axcc3  10517  axdc4uzlem  14127  hashfacen  14600  cofu1st  18059  cofu2nd  18061  cofucl  18064  fucid  18150  sursubmefmnd  19093  injsubmefmnd  19094  smndex1mgm  19107  gsumzaddlem  20136  cnfldfun  21693  cnfldfunALT  21694  znle  21843  selvval  22430  evls1fval  22638  evls1val  22639  evl1fval  22647  evl1val  22648  xkococnlem  23979  xkococn  23980  efmndtmd  24421  pserulm  26750  imsval  31288  tocycf  33679  eulerpartgbij  35005  derangenlem  35937  subfacp1lem5  35950  poimirlem9  38549  poimirlem15  38555  poimirlem17  38557  poimirlem20  38560  mbfresfi  38586  tendopl2  41836  erngplus2  41863  erngplus2-rN  41871  dvaplusgv  42069  dvhvaddass  42156  dvhlveclem  42167  diblss  42229  diblsmopel  42230  dicvaddcl  42249  dicvscacl  42250  cdlemn7  42262  dihordlem7  42273  dihopelvalcpre  42307  xihopellsmN  42313  dihopellsm  42314  rabren3dioph  43823  fzisoeu  46317  stirlinglem14  47098  fundcmpsurinjpreimafv  48491  grimco  48988  gricushgr  49016  cycldlenngric  49027  uspgrlim  49091  grlictr  49114  fuco22natlem  50454