Description: Equivalence relation with natural domain predicate, see the comment of df-ers . (Contributed by Peter Mazsa, 26-Jun-2021) (Revised by Peter Mazsa, 30-Aug-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dferALTV2 | |- ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-erALTV | |- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) ) |
|
| 2 | df-dmqs | |- ( R DomainQs A <-> ( dom R /. R ) = A ) |
|
| 3 | 2 | anbi2i | |- ( ( EqvRel R /\ R DomainQs A ) <-> ( EqvRel R /\ ( dom R /. R ) = A ) ) |
| 4 | 1 3 | bitri | |- ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) ) |