Theorem cocnv1ss

Description: Characterizing when the composition of a converse with a class is included in another. (Contributed by BJ, 22-Oct-2026)

	Ref	Expression
Assertion	cocnv1ss	⊢ ( ( ◡ 𝐵 ∘ 𝐴 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐵 𝑦 ) → 𝑥 𝐶 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		cotrg	⊢ ( ( ◡ 𝐵 ∘ 𝐴 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 ◡ 𝐵 𝑧 ) → 𝑥 𝐶 𝑧 ) )
2		vex	⊢ 𝑦 ∈ V
3		vex	⊢ 𝑧 ∈ V
4	2 3	brcnv	⊢ ( 𝑦 ◡ 𝐵 𝑧 ↔ 𝑧 𝐵 𝑦 )
5	4	anbi2i	⊢ ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 ◡ 𝐵 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐵 𝑦 ) )
6	5	imbi1i	⊢ ( ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 ◡ 𝐵 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐵 𝑦 ) → 𝑥 𝐶 𝑧 ) )
7	6	3albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 ◡ 𝐵 𝑧 ) → 𝑥 𝐶 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐵 𝑦 ) → 𝑥 𝐶 𝑧 ) )
8	1 7	bitri	⊢ ( ( ◡ 𝐵 ∘ 𝐴 ) ⊆ 𝐶 ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 𝐴 𝑦 ∧ 𝑧 𝐵 𝑦 ) → 𝑥 𝐶 𝑧 ) )