This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ V ∧ B ∈ W → A V × V ∖ R B ↔ ¬ A R B

Proof

Step Hyp Ref Expression
1 opelvvdif ⊢ A ∈ V ∧ B ∈ W → A B ∈ V × V ∖ R ↔ ¬ A B ∈ R
2 df-br ⊢ A V × V ∖ R B ↔ A B ∈ V × V ∖ R
3 df-br ⊢ A R B ↔ A B ∈ R
4 3 notbii ⊢ ¬ A R B ↔ ¬ A B ∈ R
5 1 2 4 3bitr4g ⊢ A ∈ V ∧ B ∈ W → A V × V ∖ R B ↔ ¬ A R B