Metamath Proof Explorer
Description: Existence of a difference, inference version of difexg . (Contributed by Glauco Siliprandi, 3Mar2021) (Revised by AV, 26Mar2021)


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

axmp 
⊢ ( 𝐴 ∖ 𝐵 ) ∈ V 