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

Metamath Proof Explorer

Theorem unidmqseq

Description: The union of the domain quotient of a relation is equal to the class A if and only if the range is equal to it as well. (Contributed by Peter Mazsa, 21-Apr-2019) (Revised by Peter Mazsa, 28-Dec-2021)

Ref Expression
Assertion unidmqseq ⊢ R ∈ V → Rel ⁡ R → ⋃ dom ⁡ R / R = A ↔ ran ⁡ R = A

Proof

Step Hyp Ref Expression
1 unidmqs ⊢ R ∈ V → Rel ⁡ R → ⋃ dom ⁡ R / R = ran ⁡ R
2 1 imp ⊢ R ∈ V ∧ Rel ⁡ R → ⋃ dom ⁡ R / R = ran ⁡ R
3 2 eqeq1d ⊢ R ∈ V ∧ Rel ⁡ R → ⋃ dom ⁡ R / R = A ↔ ran ⁡ R = A
4 3 ex ⊢ R ∈ V → Rel ⁡ R → ⋃ dom ⁡ R / R = A ↔ ran ⁡ R = A