Theorem disjdmqseq

Description: If a relation is disjoint, its domain quotient is equal to a class if and only if the domain quotient of the cosets by it is equal to the class. General version of eldisjn0el (which is the closest theorem to the former prter2 ). Lemma for partim2 and petlem . (Contributed by Peter Mazsa, 16-Sep-2021)

	Ref	Expression
Assertion	disjdmqseq	⊢ ( Disj 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 ↔ ( dom ≀ 𝑅 / ≀ 𝑅 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		disjdmqs	⊢ ( Disj 𝑅 → ( dom 𝑅 / 𝑅 ) = ( dom ≀ 𝑅 / ≀ 𝑅 ) )
2	1	eqeq1d	⊢ ( Disj 𝑅 → ( ( dom 𝑅 / 𝑅 ) = 𝐴 ↔ ( dom ≀ 𝑅 / ≀ 𝑅 ) = 𝐴 ) )