This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Binary equivalence relation with natural domain, see the comment of
df-ers . (Contributed by Peter Mazsa, 23-Jul-2021)
|
|
Ref |
Expression |
|
Assertion |
brers |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
df-ers |
⊢ Ers = ( DomainQss ↾ EqvRels ) |
| 2 |
1
|
eqres |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) ) |