Theorem ersymb

Description: An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypothesis	ersymb.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
Assertion	ersymb	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	⊢ ( 𝜑 → 𝑅 Er 𝑋 )
2	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝑅 Er 𝑋 )
3		simpr	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 𝑅 𝐵 )
4	2 3	ersym	⊢ ( ( 𝜑 ∧ 𝐴 𝑅 𝐵 ) → 𝐵 𝑅 𝐴 )
5	1	adantr	⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → 𝑅 Er 𝑋 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → 𝐵 𝑅 𝐴 )
7	5 6	ersym	⊢ ( ( 𝜑 ∧ 𝐵 𝑅 𝐴 ) → 𝐴 𝑅 𝐵 )
8	4 7	impbida	⊢ ( 𝜑 → ( 𝐴 𝑅 𝐵 ↔ 𝐵 𝑅 𝐴 ) )