Theorem eqvrelcoss2

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 3-May-2019)

	Ref	Expression
Assertion	eqvrelcoss2	⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqvrelcoss3	⊢ ( EqvRel ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
2		cocossss	⊢ ( ≀ ≀ 𝑅 ⊆ ≀ 𝑅 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ≀ 𝑅 𝑦 ∧ 𝑦 ≀ 𝑅 𝑧 ) → 𝑥 ≀ 𝑅 𝑧 ) )
3	1 2	bitr4i	⊢ ( EqvRel ≀ 𝑅 ↔ ≀ ≀ 𝑅 ⊆ ≀ 𝑅 )