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

Metamath Proof Explorer

Theorem eldif

Description: Expansion of membership in a class difference. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion eldif 
|- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ( B \ C ) -> A e. _V )
2 elex 
 |-  ( A e. B -> A e. _V )
3 2 adantr 
 |-  ( ( A e. B /\ -. A e. C ) -> A e. _V )
4 eleq1 
 |-  ( x = A -> ( x e. B <-> A e. B ) )
5 eleq1 
 |-  ( x = A -> ( x e. C <-> A e. C ) )
6 5 notbid 
 |-  ( x = A -> ( -. x e. C <-> -. A e. C ) )
7 4 6 anbi12d 
 |-  ( x = A -> ( ( x e. B /\ -. x e. C ) <-> ( A e. B /\ -. A e. C ) ) )
8 df-dif 
 |-  ( B \ C ) = { x | ( x e. B /\ -. x e. C ) }
9 7 8 elab2g 
 |-  ( A e. _V -> ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) ) )
10 1 3 9 pm5.21nii 
 |-  ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )