This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqvrelcoss2

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

Ref Expression
Assertion eqvrelcoss2 ⊢ EqvRel ≀ R ↔ ≀ ≀ R ⊆ ≀ R

Proof

Step Hyp Ref Expression
1 eqvrelcoss3 ⊢ EqvRel ≀ R ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
2 cocossss ⊢ ≀ ≀ R ⊆ ≀ R ↔ ∀ x ∀ y ∀ z x ≀ R y ∧ y ≀ R z → x ≀ R z
3 1 2 bitr4i ⊢ EqvRel ≀ R ↔ ≀ ≀ R ⊆ ≀ R