Metamath Proof Explorer


Theorem difexd

Description: Existence of a difference. (Contributed by SN, 16-Jul-2024)

Ref Expression
Hypothesis difexd.1 φ A V
Assertion difexd φ A B V

Proof

Step Hyp Ref Expression
1 difexd.1 φ A V
2 difexg A V A B V
3 1 2 syl φ A B V