Theorem coexd

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

	Ref	Expression
Hypotheses	coexd.1	|- ( ph -> A e. V )
	coexd.2	|- ( ph -> B e. W )
Assertion	coexd	|- ( ph -> ( A o. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		coexd.1	|- ( ph -> A e. V )
2		coexd.2	|- ( ph -> B e. W )
3		coexg	|- ( ( A e. V /\ B e. W ) -> ( A o. B ) e. _V )
4	1 2 3	syl2anc	|- ( ph -> ( A o. B ) e. _V )