Theorem coex 7637

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496   ∘ ccom 5561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568

This theorem is referenced by:  domtr  8564  enfixsn  8628  wdomtr  9041  cfcoflem  9696  axcc3  9862  axdc4uzlem  13354  hashfacen  13815  cofu1st  17155  cofu2nd  17157  cofucl  17160  fucid  17243  sursubmefmnd  18063  injsubmefmnd  18064  smndex1mgm  18074  gsumzaddlem  19043  selvval  20333  evls1fval  20484  evls1val  20485  evl1fval  20493  evl1val  20494  cnfldfun  20559  cnfldfunALT  20560  znle  20685  xkococnlem  22269  xkococn  22270  efmndtmd  22711  pserulm  25012  imsval  28464  tocycf  30761  eulerpartgbij  31632  derangenlem  32420  subfacp1lem5  32433  poimirlem9  34903  poimirlem15  34909  poimirlem17  34911  poimirlem20  34914  mbfresfi  34940  tendopl2  37915  erngplus2  37942  erngplus2-rN  37950  dvaplusgv  38148  dvhvaddass  38235  dvhlveclem  38246  diblss  38308  diblsmopel  38309  dicvaddcl  38328  dicvscacl  38329  cdlemn7  38341  dihordlem7  38352  dihopelvalcpre  38386  xihopellsmN  38392  dihopellsm  38393  rabren3dioph  39419  fzisoeu  41574  stirlinglem14  42379  fundcmpsurinjpreimafv  43575  isomushgr  43998  isomgrtr  44011