This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Peter Mazsa Equivalence relations on domain quotients dferALTV2
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 ⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
df-erALTV ⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) )
2
df-dmqs ⊢ ( 𝑅 DomainQs 𝐴 ↔ ( dom 𝑅 / 𝑅 ) = 𝐴 )
3
2
anbi2i ⊢ ( ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) ↔ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
4
1 3
bitri ⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )