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

Metamath Proof Explorer

Definition df-erALTV

Description: Equivalence relation with natural domain predicate, see also the comment of df-ers . Alternate definition is dferALTV2 . Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when A and R are sets, see brerser . (Contributed by Peter Mazsa, 12-Aug-2021)

		Ref	Expression
	Assertion	df-erALTV	⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	werALTV	⊢ 𝑅 ErALTV 𝐴
3	0	weqvrel	⊢ EqvRel 𝑅
4	1 0	wdmqs	⊢ 𝑅 DomainQs 𝐴
5	3 4	wa	⊢ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 )
6	2 5	wb	⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) )