Description: Inference from membership to difference. (Contributed by NM, 17May1998) (Proof shortened by Andrew Salmon, 26Jun2011)
Ref  Expression  

Hypothesis  difeqri.1   ( ( x e. A /\ . x e. B ) <> x e. C ) 

Assertion  difeqri   ( A \ B ) = C 
Step  Hyp  Ref  Expression 

1  difeqri.1   ( ( x e. A /\ . x e. B ) <> x e. C ) 

2  eldif   ( x e. ( A \ B ) <> ( x e. A /\ . x e. B ) ) 

3  2 1  bitri   ( x e. ( A \ B ) <> x e. C ) 
4  3  eqriv   ( A \ B ) = C 