Theorem subex

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

	Ref	Expression
Assertion	subex	⊢ − ∈ V

Proof

Step	Hyp	Ref	Expression
1		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
2		cnex	⊢ ℂ ∈ V
3	2 2	xpex	⊢ ( ℂ × ℂ ) ∈ V
4		fex2	⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ∧ ℂ ∈ V ) → − ∈ V )
5	1 3 2 4	mp3an	⊢ − ∈ V