Theorem coex 7940

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 7939	. 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 7749

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 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 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662

This theorem is used by:  domtr  9027  enfixsn  9098  wdomtr  9562  cfcoflem  10343  axcc3  10509  axdc4uzlem  14119  hashfacen  14592  cofu1st  18051  cofu2nd  18053  cofucl  18056  fucid  18142  sursubmefmnd  19085  injsubmefmnd  19086  smndex1mgm  19099  gsumzaddlem  20128  cnfldfun  21685  cnfldfunALT  21686  znle  21835  selvval  22422  evls1fval  22630  evls1val  22631  evl1fval  22639  evl1val  22640  xkococnlem  23971  xkococn  23972  efmndtmd  24413  pserulm  26742  imsval  31280  tocycf  33671  eulerpartgbij  34997  derangenlem  35915  subfacp1lem5  35928  poimirlem9  38527  poimirlem15  38533  poimirlem17  38535  poimirlem20  38538  mbfresfi  38564  tendopl2  41814  erngplus2  41841  erngplus2-rN  41849  dvaplusgv  42047  dvhvaddass  42134  dvhlveclem  42145  diblss  42207  diblsmopel  42208  dicvaddcl  42227  dicvscacl  42228  cdlemn7  42240  dihordlem7  42251  dihopelvalcpre  42285  xihopellsmN  42291  dihopellsm  42292  rabren3dioph  43801  fzisoeu  46285  stirlinglem14  47066  fundcmpsurinjpreimafv  48459  grimco  48956  gricushgr  48984  cycldlenngric  48995  uspgrlim  49059  grlictr  49082  fuco22natlem  50422