Theorem brvdif2

Description: Binary relation with universal complement. (Contributed by Peter Mazsa, 14-Jul-2018)

	Ref	Expression
Assertion	brvdif2	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		brvdif	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ¬ 𝐴 𝑅 𝐵 )
2		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
3	1 2	xchbinx	⊢ ( 𝐴 ( V ∖ 𝑅 ) 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )