Metamath Proof Explorer

Theorem brvdif

Description: Binary relation with universal complement is the negation of the relation. (Contributed by Peter Mazsa, 1-Jul-2018)

Ref Expression
Assertion brvdif 
|- ( A ( _V \ R ) B <-> -. A R B )

Proof

Step Hyp Ref Expression
1 brv 
 |-  A _V B
2 brdif 
 |-  ( A ( _V \ R ) B <-> ( A _V B /\ -. A R B ) )
3 1 2 mpbiran 
 |-  ( A ( _V \ R ) B <-> -. A R B )