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 e. _V
Assertion	difexi	|- ( A \ B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		difexi.1	|- A e. _V
2		difexg	|- ( A e. _V -> ( A \ B ) e. _V )
3	1 2	ax-mp	|- ( A \ B ) e. _V