Theorem disjdmqs 38912

Description: If a relation is disjoint, its domain quotient is equal to the domain quotient of the cosets by it. Lemma for partim2 38915 and petlem 38920 via disjdmqseq 38913. (Contributed by Peter Mazsa, 16-Sep-2021.)

Assertion

Ref	Expression
disjdmqs	⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))

Proof of Theorem disjdmqs

Step	Hyp	Ref	Expression
1		disjdmqsss 38910	. 2 ⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) ⊆ (dom ≀ 𝑅 / ≀ 𝑅))
2		disjdmqscossss 38911	. 2 ⊢ ( Disj 𝑅 → (dom ≀ 𝑅 / ≀ 𝑅) ⊆ (dom 𝑅 / 𝑅))
3	1, 2	eqssd 3949	1 ⊢ ( Disj 𝑅 → (dom 𝑅 / 𝑅) = (dom ≀ 𝑅 / ≀ 𝑅))

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5621   / cqs 8630   ≀ ccoss 38232   Disj wdisjALTV 38266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2883  df-ral 3050  df-rex 3059  df-rmo 3348  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-ec 8633  df-qs 8637  df-coss 38523  df-cnvrefrel 38629  df-disjALTV 38813

This theorem is referenced by:  disjdmqseq  38913