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 Domain quotients brdmqssqs
Description: If A and R are sets, the domain quotient binary relation and the
domain quotient predicate are the same. (Contributed by Peter Mazsa , 14-Aug-2021)
Ref
Expression
Assertion
brdmqssqs ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴 ) )
Proof
Step
Hyp
Ref
Expression
1
brdmqss ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 DomainQss 𝐴 ↔ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
2
df-dmqs ⊢ ( 𝑅 DomainQs 𝐴 ↔ ( dom 𝑅 / 𝑅 ) = 𝐴 )
3
1 2
bitr4di ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴 ) )