Theorem detinidres 38738

Description: The cosets by the intersection with the restricted identity relation are in equivalence relation if and only if the intersection with the restricted identity relation is disjoint. (Contributed by Peter Mazsa, 31-Dec-2021.)

Assertion

Ref	Expression
detinidres	⊢ ( Disj (𝑅 ∩ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)))

Proof of Theorem detinidres

Step	Hyp	Ref	Expression
1		disjALTVinidres 38699	. 2 ⊢ Disj (𝑅 ∩ ( I ↾ 𝐴))
2	1	detlem 38725	1 ⊢ ( Disj (𝑅 ∩ ( I ↾ 𝐴)) ↔ EqvRel ≀ (𝑅 ∩ ( I ↾ 𝐴)))

Syntax hints:   ↔ wb 206   ∩ cin 3932   I cid 5559   ↾ cres 5669   ≀ ccoss 38123   EqvRel weqvrel 38140   Disj wdisjALTV 38157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-opab 5188  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-coss 38353  df-refrel 38454  df-cnvrefrel 38469  df-symrel 38486  df-trrel 38516  df-eqvrel 38527  df-funALTV 38624  df-disjALTV 38647

This theorem is referenced by: (None)