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	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ¬ 𝐴 𝑅 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		brv	⊢ 𝐴 V 𝐵
2		brdif	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ( 𝐴 V 𝐵 ∧ ¬ 𝐴 𝑅 𝐵 ) )
3	1 2	mpbiran	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ¬ 𝐴 𝑅 𝐵 )