Theorem brnonrel

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

	Ref	Expression
Assertion	brnonrel	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		br0	⊢ ¬ 𝑌 ∅ 𝑋
2		brcnvg	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝑈 ) → ( 𝑌 ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑋 ↔ 𝑋 ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑌 ) )
3	2	ancoms	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑌 ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑋 ↔ 𝑋 ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑌 ) )
4		cnvnonrel	⊢ ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅
5	4	breqi	⊢ ( 𝑌 ◡ ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑋 ↔ 𝑌 ∅ 𝑋 )
6	3 5	bitr3di	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑌 ↔ 𝑌 ∅ 𝑋 ) )
7	1 6	mtbiri	⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ) → ¬ 𝑋 ( 𝐴 ∖ ◡ ◡ 𝐴 ) 𝑌 )