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	⊢ ( 𝜑 → EqvRel 𝑅 )
	eqvrelcl.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
Assertion	eqvrelcl	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqvrelcl.1	⊢ ( 𝜑 → EqvRel 𝑅 )
2		eqvrelcl.2	⊢ ( 𝜑 → 𝐴 𝑅 𝐵 )
3		eqvrelrel	⊢ ( EqvRel 𝑅 → Rel 𝑅 )
4	1 3	syl	⊢ ( 𝜑 → Rel 𝑅 )
5		releldm	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ dom 𝑅 )
6	4 2 5	syl2anc	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑅 )