Theorem 0er

Description: The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015) (Proof shortened by AV, 1-May-2021)

	Ref	Expression
Assertion	0er	⊢ ∅ Er ∅

Proof

Step	Hyp	Ref	Expression
1		rel0	⊢ Rel ∅
2		df-br	⊢ ( 𝑥 ∅ 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ )
3		noel	⊢ ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅
4	3	pm2.21i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ → 𝑦 ∅ 𝑥 )
5	2 4	sylbi	⊢ ( 𝑥 ∅ 𝑦 → 𝑦 ∅ 𝑥 )
6	3	pm2.21i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ → 𝑥 ∅ 𝑧 )
7	2 6	sylbi	⊢ ( 𝑥 ∅ 𝑦 → 𝑥 ∅ 𝑧 )
8	7	adantr	⊢ ( ( 𝑥 ∅ 𝑦 ∧ 𝑦 ∅ 𝑧 ) → 𝑥 ∅ 𝑧 )
9		noel	⊢ ¬ 𝑥 ∈ ∅
10		noel	⊢ ¬ ⟨ 𝑥 , 𝑥 ⟩ ∈ ∅
11	9 10	2false	⊢ ( 𝑥 ∈ ∅ ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ∅ )
12		df-br	⊢ ( 𝑥 ∅ 𝑥 ↔ ⟨ 𝑥 , 𝑥 ⟩ ∈ ∅ )
13	11 12	bitr4i	⊢ ( 𝑥 ∈ ∅ ↔ 𝑥 ∅ 𝑥 )
14	1 5 8 13	iseri	⊢ ∅ Er ∅