Metamath Proof Explorer

Theorem cossssid3

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 cossssid3 ⊢ ≀ R ⊆ I ↔ ∀ u ∀ x ∀ y u R x ∧ u R y → x = y

Proof

Step Hyp Ref Expression
1 cossssid2 ⊢ ≀ R ⊆ I ↔ ∀ x ∀ y ∃ u u R x ∧ u R y → x = y
2 19.23v ⊢ ∀ u u R x ∧ u R y → x = y ↔ ∃ u u R x ∧ u R y → x = y
3 2 albii ⊢ ∀ y ∀ u u R x ∧ u R y → x = y ↔ ∀ y ∃ u u R x ∧ u R y → x = y
4 alcom ⊢ ∀ y ∀ u u R x ∧ u R y → x = y ↔ ∀ u ∀ y u R x ∧ u R y → x = y
5 3 4 bitr3i ⊢ ∀ y ∃ u u R x ∧ u R y → x = y ↔ ∀ u ∀ y u R x ∧ u R y → x = y
6 5 albii ⊢ ∀ x ∀ y ∃ u u R x ∧ u R y → x = y ↔ ∀ x ∀ u ∀ y u R x ∧ u R y → x = y
7 alcom ⊢ ∀ x ∀ u ∀ y u R x ∧ u R y → x = y ↔ ∀ u ∀ x ∀ y u R x ∧ u R y → x = y
8 1 6 7 3bitri ⊢ ≀ R ⊆ I ↔ ∀ u ∀ x ∀ y u R x ∧ u R y → x = y