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

Metamath Proof Explorer

Theorem iseriALT

Description: Alternate proof of iseri , avoiding the usage of mptru and T. as antecedent by using ax-mp and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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 iseriALT 
|- 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 id 
 |-  ( Rel R -> Rel R )
6 2 adantl 
 |-  ( ( Rel R /\ x R y ) -> y R x )
7 3 adantl 
 |-  ( ( Rel R /\ ( x R y /\ y R z ) ) -> x R z )
8 4 a1i 
 |-  ( Rel R -> ( x e. A <-> x R x ) )
9 5 6 7 8 iserd 
 |-  ( Rel R -> R Er A )
10 1 9 ax-mp 
 |-  R Er A