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	⊢ 𝐴 ∈ V
Assertion	difexi	⊢ ( 𝐴 ∖ 𝐵 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		difexi.1	⊢ 𝐴 ∈ V
2		difexg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ 𝐵 ) ∈ V )
3	1 2	ax-mp	⊢ ( 𝐴 ∖ 𝐵 ) ∈ V