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	$⊢ R ErALTV A \leftrightarrow (EqvRel R \land R DomainQs A)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	werALTV	$wff R ErALTV A$
3	0	weqvrel	$wff EqvRel R$
4	1 0	wdmqs	$wff R DomainQs A$
5	3 4	wa	$wff (EqvRel R \land R DomainQs A)$
6	2 5	wb	$wff (R ErALTV A \leftrightarrow (EqvRel R \land R DomainQs A))$