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 \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	iseriALT	$⊢ 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		id	$⊢ Rel R \to Rel R$
6	2	adantl	$⊢ (Rel R \land x R y) \to y R x$
7	3	adantl	$⊢ (Rel R \land (x R y \land y R z)) \to x R z$
8	4	a1i	$⊢ Rel R \to (x \in A \leftrightarrow x R x)$
9	5 6 7 8	iserd	$⊢ Rel R \to R Er A$
10	1 9	ax-mp	$⊢ R Er A$