Metamath Proof Explorer

Theorem iseri

Description: A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd , which avoids the need to provide a "dummy antecedent" ph if there is no natural one to choose. (Contributed by AV, 30-Apr-2021)

	Ref	Expression
Hypotheses	iseri.1	$⊢ Rel R$
	iseri.2	$⊢ x R y \to y R x$
	iseri.3	$⊢ (x R y \land y R z) \to x R z$
	iseri.4	$⊢ x \in A \leftrightarrow x R x$
Assertion	iseri	$⊢ R Er A$

Proof

Step	Hyp	Ref	Expression
1		iseri.1	$⊢ Rel R$
2		iseri.2	$⊢ x R y \to y R x$
3		iseri.3	$⊢ (x R y \land y R z) \to x R z$
4		iseri.4	$⊢ x \in A \leftrightarrow x R x$
5	1	a1i	$⊢ ⊤ \to Rel R$
6	2	adantl	$⊢ (⊤ \land x R y) \to y R x$
7	3	adantl	$⊢ (⊤ \land (x R y \land y R z)) \to x R z$
8	4	a1i	$⊢ ⊤ \to (x \in A \leftrightarrow x R x)$
9	5 6 7 8	iserd	$⊢ ⊤ \to R Er A$
10	9	mptru	$⊢ R Er A$