Theorem relnonrel

Description: The non-relation part of a relation is empty. (Contributed by RP, 22-Oct-2020)

	Ref	Expression
Assertion	relnonrel	⊢ ( Rel 𝐴 ↔ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		dfrel2	⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
2		eqss	⊢ ( ◡ ◡ 𝐴 = 𝐴 ↔ ( ◡ ◡ 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ◡ ◡ 𝐴 ) )
3	1 2	bitri	⊢ ( Rel 𝐴 ↔ ( ◡ ◡ 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ◡ ◡ 𝐴 ) )
4		cnvcnvss	⊢ ◡ ◡ 𝐴 ⊆ 𝐴
5	4	biantrur	⊢ ( 𝐴 ⊆ ◡ ◡ 𝐴 ↔ ( ◡ ◡ 𝐴 ⊆ 𝐴 ∧ 𝐴 ⊆ ◡ ◡ 𝐴 ) )
6		ssdif0	⊢ ( 𝐴 ⊆ ◡ ◡ 𝐴 ↔ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅ )
7	3 5 6	3bitr2i	⊢ ( Rel 𝐴 ↔ ( 𝐴 ∖ ◡ ◡ 𝐴 ) = ∅ )