Metamath Proof Explorer

Theorem difexi

Description: Existence of a difference, inference version of difexg . (Contributed by Glauco Siliprandi, 3-Mar-2021) (Revised by AV, 26-Mar-2021)

Ref Expression
Hypothesis difexi.1 A V
Assertion difexi A B V


Step Hyp Ref Expression
1 difexi.1 A V
2 difexg A V A B V
3 1 2 ax-mp A B V