Theorem dfrel2

Description: Alternate definition of relation. Exercise 2 of TakeutiZaring p. 25. (Contributed by NM, 29-Dec-1996)

	Ref	Expression
Assertion	dfrel2	⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		relcnv	⊢ Rel ◡ ◡ 𝑅
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	opelcnv	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ◡ 𝑅 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 )
5	3 2	opelcnv	⊢ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
6	4 5	bitri	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ◡ ◡ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
7	6	eqrelriv	⊢ ( ( Rel ◡ ◡ 𝑅 ∧ Rel 𝑅 ) → ◡ ◡ 𝑅 = 𝑅 )
8	1 7	mpan	⊢ ( Rel 𝑅 → ◡ ◡ 𝑅 = 𝑅 )
9		releq	⊢ ( ◡ ◡ 𝑅 = 𝑅 → ( Rel ◡ ◡ 𝑅 ↔ Rel 𝑅 ) )
10	1 9	mpbii	⊢ ( ◡ ◡ 𝑅 = 𝑅 → Rel 𝑅 )
11	8 10	impbii	⊢ ( Rel 𝑅 ↔ ◡ ◡ 𝑅 = 𝑅 )