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 <-> ( EqvRel R /\ R DomainQs A ) )

Detailed syntax breakdown


 |-  R
 |-  A
 |-  R ErALTV A
 |-  EqvRel R
 |-  R DomainQs A
 |-  ( EqvRel R /\ R DomainQs A )
 |-  ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) )

Step	Hyp	Ref	Expression
0		cR	\|- R
1		cA	\|- A
2	1 0	werALTV	\|- R ErALTV A
3	0	weqvrel	\|- EqvRel R
4	1 0	wdmqs	\|- R DomainQs A
5	3 4	wa	\|- ( EqvRel R /\ R DomainQs A )
6	2 5	wb	\|- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) )