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

Detailed syntax breakdown

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 ) )