Metamath Proof Explorer

Theorem velcomp

Description: Characterization of setvar elements of the complement of a class. (Contributed by Andrew Salmon, 15-Jul-2011)

Ref Expression
Assertion velcomp 
|- ( x e. ( _V \ A ) <-> -. x e. A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 eldif 
 |-  ( x e. ( _V \ A ) <-> ( x e. _V /\ -. x e. A ) )
3 1 2 mpbiran 
 |-  ( x e. ( _V \ A ) <-> -. x e. A )