Theorem coex

Description: The composition of two sets is a set. (Contributed by NM, 15-Dec-2003)

	Ref	Expression
Hypotheses	coex.1	$$⊢A\in \mathrm{V}$$
	coex.2	$$⊢B\in \mathrm{V}$$
Assertion	coex	$$⊢A\circ B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		coex.1	$$⊢A\in \mathrm{V}$$
2		coex.2	$$⊢B\in \mathrm{V}$$
3		coexg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to A\circ B\in \mathrm{V}$$
4	1 2 3	mp2an	$$⊢A\circ B\in \mathrm{V}$$