This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 -> 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