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 𝑅
	iseri.2	⊢ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 )
	iseri.3	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
	iseri.4	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 )
Assertion	iseri	⊢ 𝑅 Er 𝐴

Proof

Step	Hyp	Ref	Expression
1		iseri.1	⊢ Rel 𝑅
2		iseri.2	⊢ ( 𝑥 𝑅 𝑦 → 𝑦 𝑅 𝑥 )
3		iseri.3	⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
4		iseri.4	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 )
5	1	a1i	⊢ ( ⊤ → Rel 𝑅 )
6	2	adantl	⊢ ( ( ⊤ ∧ 𝑥 𝑅 𝑦 ) → 𝑦 𝑅 𝑥 )
7	3	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ) → 𝑥 𝑅 𝑧 )
8	4	a1i	⊢ ( ⊤ → ( 𝑥 ∈ 𝐴 ↔ 𝑥 𝑅 𝑥 ) )
9	5 6 7 8	iserd	⊢ ( ⊤ → 𝑅 Er 𝐴 )
10	9	mptru	⊢ 𝑅 Er 𝐴