# Metamath Proof Explorer

## Theorem vtoclr

Description: Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses vtoclr.1 ${⊢}\mathrm{Rel}{R}$
vtoclr.2 ${⊢}\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}$
Assertion vtoclr ${⊢}\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}$

### Proof

Step Hyp Ref Expression
1 vtoclr.1 ${⊢}\mathrm{Rel}{R}$
2 vtoclr.2 ${⊢}\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}$
3 1 brrelex12i ${⊢}{A}{R}{B}\to \left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
4 1 brrelex2i ${⊢}{B}{R}{C}\to {C}\in \mathrm{V}$
5 breq1 ${⊢}{x}={A}\to \left({x}{R}{y}↔{A}{R}{y}\right)$
6 5 anbi1d ${⊢}{x}={A}\to \left(\left({x}{R}{y}\wedge {y}{R}{C}\right)↔\left({A}{R}{y}\wedge {y}{R}{C}\right)\right)$
7 breq1 ${⊢}{x}={A}\to \left({x}{R}{C}↔{A}{R}{C}\right)$
8 6 7 imbi12d ${⊢}{x}={A}\to \left(\left(\left({x}{R}{y}\wedge {y}{R}{C}\right)\to {x}{R}{C}\right)↔\left(\left({A}{R}{y}\wedge {y}{R}{C}\right)\to {A}{R}{C}\right)\right)$
9 8 imbi2d ${⊢}{x}={A}\to \left(\left({C}\in \mathrm{V}\to \left(\left({x}{R}{y}\wedge {y}{R}{C}\right)\to {x}{R}{C}\right)\right)↔\left({C}\in \mathrm{V}\to \left(\left({A}{R}{y}\wedge {y}{R}{C}\right)\to {A}{R}{C}\right)\right)\right)$
10 breq2 ${⊢}{y}={B}\to \left({A}{R}{y}↔{A}{R}{B}\right)$
11 breq1 ${⊢}{y}={B}\to \left({y}{R}{C}↔{B}{R}{C}\right)$
12 10 11 anbi12d ${⊢}{y}={B}\to \left(\left({A}{R}{y}\wedge {y}{R}{C}\right)↔\left({A}{R}{B}\wedge {B}{R}{C}\right)\right)$
13 12 imbi1d ${⊢}{y}={B}\to \left(\left(\left({A}{R}{y}\wedge {y}{R}{C}\right)\to {A}{R}{C}\right)↔\left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)\right)$
14 13 imbi2d ${⊢}{y}={B}\to \left(\left({C}\in \mathrm{V}\to \left(\left({A}{R}{y}\wedge {y}{R}{C}\right)\to {A}{R}{C}\right)\right)↔\left({C}\in \mathrm{V}\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)\right)\right)$
15 breq2 ${⊢}{z}={C}\to \left({y}{R}{z}↔{y}{R}{C}\right)$
16 15 anbi2d ${⊢}{z}={C}\to \left(\left({x}{R}{y}\wedge {y}{R}{z}\right)↔\left({x}{R}{y}\wedge {y}{R}{C}\right)\right)$
17 breq2 ${⊢}{z}={C}\to \left({x}{R}{z}↔{x}{R}{C}\right)$
18 16 17 imbi12d ${⊢}{z}={C}\to \left(\left(\left({x}{R}{y}\wedge {y}{R}{z}\right)\to {x}{R}{z}\right)↔\left(\left({x}{R}{y}\wedge {y}{R}{C}\right)\to {x}{R}{C}\right)\right)$
19 18 2 vtoclg ${⊢}{C}\in \mathrm{V}\to \left(\left({x}{R}{y}\wedge {y}{R}{C}\right)\to {x}{R}{C}\right)$
20 9 14 19 vtocl2g ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\to \left({C}\in \mathrm{V}\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)\right)$
21 3 4 20 syl2im ${⊢}{A}{R}{B}\to \left({B}{R}{C}\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)\right)$
22 21 imp ${⊢}\left({A}{R}{B}\wedge {B}{R}{C}\right)\to \left(\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}\right)$
23 22 pm2.43i ${⊢}\left({A}{R}{B}\wedge {B}{R}{C}\right)\to {A}{R}{C}$