Metamath Proof Explorer


Theorem difexd

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

Ref Expression
Hypothesis difexd.1 ( 𝜑𝐴𝑉 )
Assertion difexd ( 𝜑 → ( 𝐴𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 difexd.1 ( 𝜑𝐴𝑉 )
2 difexg ( 𝐴𝑉 → ( 𝐴𝐵 ) ∈ V )
3 1 2 syl ( 𝜑 → ( 𝐴𝐵 ) ∈ V )