Theorem brnonrel

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

	Ref	Expression
Assertion	brnonrel	|- ( ( X e. U /\ Y e. V ) -> -. X ( A \ `' `' A ) Y )

Proof

Step	Hyp	Ref	Expression
1		br0	|- -. Y (/) X
2		brcnvg	|- ( ( Y e. V /\ X e. U ) -> ( Y `' ( A \ `' `' A ) X <-> X ( A \ `' `' A ) Y ) )
3	2	ancoms	|- ( ( X e. U /\ Y e. V ) -> ( Y `' ( A \ `' `' A ) X <-> X ( A \ `' `' A ) Y ) )
4		cnvnonrel	|- `' ( A \ `' `' A ) = (/)
5	4	breqi	|- ( Y `' ( A \ `' `' A ) X <-> Y (/) X )
6	3 5	bitr3di	|- ( ( X e. U /\ Y e. V ) -> ( X ( A \ `' `' A ) Y <-> Y (/) X ) )
7	1 6	mtbiri	|- ( ( X e. U /\ Y e. V ) -> -. X ( A \ `' `' A ) Y )