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

Metamath Proof Explorer

Theorem eqvrelcl

Description: Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 2-Jun-2019)

	Ref	Expression
Hypotheses	eqvrelcl.1	$⊢ φ \to EqvRel R$
	eqvrelcl.2	$⊢ φ \to A R B$
Assertion	eqvrelcl	$⊢ φ \to A \in dom R$

Proof

Step	Hyp	Ref	Expression
1		eqvrelcl.1	$⊢ φ \to EqvRel R$
2		eqvrelcl.2	$⊢ φ \to A R B$
3		eqvrelrel	$⊢ EqvRel R \to Rel R$
4	1 3	syl	$⊢ φ \to Rel R$
5		releldm	$⊢ (Rel R \land A R B) \to A \in dom R$
6	4 2 5	syl2anc	$⊢ φ \to A \in dom R$