Theorem cossssid2

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019)

	Ref	Expression
Assertion	cossssid2	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		df-id	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
2	1	sseq2i	⊢ ( ≀ 𝑅 ⊆ I ↔ ≀ 𝑅 ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } )
3		df-coss	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
4	3	sseq1i	⊢ ( ≀ 𝑅 ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } )
5		ssopab2bw	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } ↔ ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )
6	2 4 5	3bitri	⊢ ( ≀ 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) → 𝑥 = 𝑦 ) )