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