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