# Metamath Proof Explorer

## Theorem brnonrel

Description: A non-relation cannot relate any two classes. (Contributed by RP, 23-Oct-2020)

Ref Expression
Assertion brnonrel ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\right)\to ¬{X}\left({A}\setminus {{{A}}^{-1}}^{-1}\right){Y}$

### Proof

Step Hyp Ref Expression
1 br0 ${⊢}¬{Y}\varnothing {X}$
2 brcnvg ${⊢}\left({Y}\in {V}\wedge {X}\in {U}\right)\to \left({Y}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)}^{-1}{X}↔{X}\left({A}\setminus {{{A}}^{-1}}^{-1}\right){Y}\right)$
3 2 ancoms ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\right)\to \left({Y}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)}^{-1}{X}↔{X}\left({A}\setminus {{{A}}^{-1}}^{-1}\right){Y}\right)$
4 cnvnonrel ${⊢}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)}^{-1}=\varnothing$
5 4 breqi ${⊢}{Y}{\left({A}\setminus {{{A}}^{-1}}^{-1}\right)}^{-1}{X}↔{Y}\varnothing {X}$
6 3 5 bitr3di ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\right)\to \left({X}\left({A}\setminus {{{A}}^{-1}}^{-1}\right){Y}↔{Y}\varnothing {X}\right)$
7 1 6 mtbiri ${⊢}\left({X}\in {U}\wedge {Y}\in {V}\right)\to ¬{X}\left({A}\setminus {{{A}}^{-1}}^{-1}\right){Y}$