Metamath Proof Explorer


Theorem brvvdif

Description: Binary relation with the complement under the universal class of ordered pairs. (Contributed by Peter Mazsa, 9-Nov-2018)

Ref Expression
Assertion brvvdif ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( ( V × V ) ∖ 𝑅 ) 𝐵 ↔ ¬ 𝐴 𝑅 𝐵 ) )

Proof

Step Hyp Ref Expression
1 opelvvdif ( ( 𝐴𝑉𝐵𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( V × V ) ∖ 𝑅 ) ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 ) )
2 df-br ( 𝐴 ( ( V × V ) ∖ 𝑅 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ( V × V ) ∖ 𝑅 ) )
3 df-br ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
4 3 notbii ( ¬ 𝐴 𝑅 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
5 1 2 4 3bitr4g ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 ( ( V × V ) ∖ 𝑅 ) 𝐵 ↔ ¬ 𝐴 𝑅 𝐵 ) )