Theorem subex

Description: The subtraction operation is a set. (Contributed by SN, 5-Jun-2025)

	Ref	Expression
Assertion	subex	$$⊢-\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3	2 2	xpex	$$⊢ℂ\times ℂ\in \mathrm{V}$$
4		fex2	$$⊢\left(-:ℂ\times ℂ⟶ℂ\wedge ℂ\times ℂ\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to -\in \mathrm{V}$$
5	1 3 2 4	mp3an	$$⊢-\in \mathrm{V}$$