Theorem coexd

Description: The composition of two sets is a set. (Contributed by SN, 7-Feb-2025)

	Ref	Expression
Hypotheses	coexd.1	$$⊢\phi \to A\in V$$
	coexd.2	$$⊢\phi \to B\in W$$
Assertion	coexd	$$⊢\phi \to A\circ B\in \mathrm{V}$$

Proof

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