erref

Description: An equivalence relation is reflexive on its field. Compare Theorem 3M of Enderton p. 56. (Contributed by Mario Carneiro, 6-May-2013) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	ersymb.1	$⊢ φ \to R Er X$
	erref.2	$⊢ φ \to A \in X$
Assertion	erref	$⊢ φ \to A R A$

Proof

Step	Hyp	Ref	Expression
1		ersymb.1	$⊢ φ \to R Er X$
2		erref.2	$⊢ φ \to A \in X$
3		erdm	$⊢ R Er X \to dom R = X$
4	1 3	syl	$⊢ φ \to dom R = X$
5	2 4	eleqtrrd	$⊢ φ \to A \in dom R$
6		eldmg	$⊢ A \in X \to (A \in dom R \leftrightarrow \exists x A R x)$
7	2 6	syl	$⊢ φ \to (A \in dom R \leftrightarrow \exists x A R x)$
8	5 7	mpbid	$⊢ φ \to \exists x A R x$
9	1	adantr	$⊢ (φ \land A R x) \to R Er X$
10		simpr	$⊢ (φ \land A R x) \to A R x$
11	9 10 10	ertr4d	$⊢ (φ \land A R x) \to A R A$
12	8 11	exlimddv	$⊢ φ \to A R A$

Metamath Proof Explorer

Theorem erref

Proof