Metamath Proof Explorer

Theorem difeqri

Description: Inference from membership to difference. (Contributed by NM, 17-May-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Hypothesis difeqri.1 
|- ( ( x e. A /\ -. x e. B ) <-> x e. C )
Assertion difeqri 
|- ( A \ B ) = C

Proof

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