Theorem difexd

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

	Ref	Expression
Hypothesis	difexd.1	|- ( ph -> A e. V )
Assertion	difexd	|- ( ph -> ( A \ B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		difexd.1	|- ( ph -> A e. V )
2		difexg	|- ( A e. V -> ( A \ B ) e. _V )
3	1 2	syl	|- ( ph -> ( A \ B ) e. _V )