This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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