Metamath Proof Explorer

Theorem subex

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

Ref Expression
Assertion subex 
|- - e. _V

Proof

Step Hyp Ref Expression
1 subf 
 |-  - : ( CC X. CC ) --> CC
2 cnex 
 |-  CC e. _V
3 2 2 xpex 
 |-  ( CC X. CC ) e. _V
4 fex2 
 |-  ( ( - : ( CC X. CC ) --> CC /\ ( CC X. CC ) e. _V /\ CC e. _V ) -> - e. _V )
5 1 3 2 4 mp3an 
 |-  - e. _V