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	$$⊢\varnothing \mathrm{Er}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		rel0	$$⊢\mathrm{Rel}\varnothing$$
2		df-br	$$⊢x\varnothing y\leftrightarrow ⟨x,y⟩\in \varnothing$$
3		noel	$$⊢\neg ⟨x,y⟩\in \varnothing$$
4	3	pm2.21i	$$⊢⟨x,y⟩\in \varnothing \to y\varnothing x$$
5	2 4	sylbi	$$⊢x\varnothing y\to y\varnothing x$$
6	3	pm2.21i	$$⊢⟨x,y⟩\in \varnothing \to x\varnothing z$$
7	2 6	sylbi	$$⊢x\varnothing y\to x\varnothing z$$
8	7	adantr	$$⊢\left(x\varnothing y\wedge y\varnothing z\right)\to x\varnothing z$$
9		noel	$$⊢\neg x\in \varnothing$$
10		noel	$$⊢\neg ⟨x,x⟩\in \varnothing$$
11	9 10	2false	$$⊢x\in \varnothing \leftrightarrow ⟨x,x⟩\in \varnothing$$
12		df-br	$$⊢x\varnothing x\leftrightarrow ⟨x,x⟩\in \varnothing$$
13	11 12	bitr4i	$$⊢x\in \varnothing \leftrightarrow x\varnothing x$$
14	1 5 8 13	iseri	$$⊢\varnothing \mathrm{Er}\varnothing$$