Metamath Proof Explorer

Theorem cocnv2ssid

Description: Characterizing when the composition of a class with a converse is included in the identity relation. The instance where the two classes are equal gives a characterization of single-valuedness (that is, for a relation to be a function, see df-fun ). (Contributed by BJ, 22-Oct-2026)

Ref Expression
Assertion cocnv2ssid ⊢ B ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x = z

Proof

Step Hyp Ref Expression
1 cocnv2ss ⊢ B ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x I z
2 vex ⊢ z ∈ V
3 2 ideq ⊢ x I z ↔ x = z
4 3 imbi2i ⊢ y A x ∧ y B z → x I z ↔ y A x ∧ y B z → x = z
5 4 3albii ⊢ ∀ x ∀ y ∀ z y A x ∧ y B z → x I z ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x = z
6 1 5 bitri ⊢ B ∘ A -1 ⊆ I ↔ ∀ x ∀ y ∀ z y A x ∧ y B z → x = z