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 -> y R x )
	iseri.3	|- ( ( x R y /\ y R z ) -> x R z )
	iseri.4	|- ( x e. A <-> x R x )
Assertion	iseri	|- R Er A

Proof

Step	Hyp	Ref	Expression
1		iseri.1	|- Rel R
2		iseri.2	|- ( x R y -> y R x )
3		iseri.3	|- ( ( x R y /\ y R z ) -> x R z )
4		iseri.4	|- ( x e. A <-> x R x )
5	1	a1i	|- ( T. -> Rel R )
6	2	adantl	|- ( ( T. /\ x R y ) -> y R x )
7	3	adantl	|- ( ( T. /\ ( x R y /\ y R z ) ) -> x R z )
8	4	a1i	|- ( T. -> ( x e. A <-> x R x ) )
9	5 6 7 8	iserd	|- ( T. -> R Er A )
10	9	mptru	|- R Er A