This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brdmqss

Description: The domain quotient binary relation. (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Assertion brdmqss ⊢ A ∈ V ∧ R ∈ W → R DomainQss A ↔ dom ⁡ R / R = A

Proof

Step Hyp Ref Expression
1 dmqseq ⊢ x = R → dom ⁡ x / x = dom ⁡ R / R
2 id ⊢ y = A → y = A
3 1 2 eqeqan12d ⊢ x = R ∧ y = A → dom ⁡ x / x = y ↔ dom ⁡ R / R = A
4 df-dmqss ⊢ DomainQss = x y | dom ⁡ x / x = y
5 3 4 brabga ⊢ R ∈ W ∧ A ∈ V → R DomainQss A ↔ dom ⁡ R / R = A
6 5 ancoms ⊢ A ∈ V ∧ R ∈ W → R DomainQss A ↔ dom ⁡ R / R = A