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	⊢ ( ( 𝐵 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		cocnv2ss	⊢ ( ( 𝐵 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 I 𝑧 ) )
2		vex	⊢ 𝑧 ∈ V
3	2	ideq	⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
4	3	imbi2i	⊢ ( ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 I 𝑧 ) ↔ ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 = 𝑧 ) )
5	4	3albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 I 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 = 𝑧 ) )
6	1 5	bitri	⊢ ( ( 𝐵 ∘ ◡ 𝐴 ) ⊆ I ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 𝐴 𝑥 ∧ 𝑦 𝐵 𝑧 ) → 𝑥 = 𝑧 ) )