This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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