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 ⊢Rel⁡R
vtoclr.2 ⊢xRy∧yRz→xRz
Assertion vtoclr ⊢ARB∧BRC→ARC

Proof

Step Hyp Ref Expression
1 vtoclr.1 ⊢Rel⁡R
2 vtoclr.2 ⊢xRy∧yRz→xRz
3 1 brrelex12i ⊢ARB→A∈V∧B∈V
4 1 brrelex2i ⊢BRC→C∈V
5 breq1 ⊢x=A→xRy↔ARy
6 5 anbi1d ⊢x=A→xRy∧yRC↔ARy∧yRC
7 breq1 ⊢x=A→xRC↔ARC
8 6 7 imbi12d ⊢x=A→xRy∧yRC→xRC↔ARy∧yRC→ARC
9 8 imbi2d ⊢x=A→C∈V→xRy∧yRC→xRC↔C∈V→ARy∧yRC→ARC
10 breq2 ⊢y=B→ARy↔ARB
11 breq1 ⊢y=B→yRC↔BRC
12 10 11 anbi12d ⊢y=B→ARy∧yRC↔ARB∧BRC
13 12 imbi1d ⊢y=B→ARy∧yRC→ARC↔ARB∧BRC→ARC
14 13 imbi2d ⊢y=B→C∈V→ARy∧yRC→ARC↔C∈V→ARB∧BRC→ARC
15 breq2 ⊢z=C→yRz↔yRC
16 15 anbi2d ⊢z=C→xRy∧yRz↔xRy∧yRC
17 breq2 ⊢z=C→xRz↔xRC
18 16 17 imbi12d ⊢z=C→xRy∧yRz→xRz↔xRy∧yRC→xRC
19 18 2 vtoclg ⊢C∈V→xRy∧yRC→xRC
20 9 14 19 vtocl2g ⊢A∈V∧B∈V→C∈V→ARB∧BRC→ARC
21 3 4 20 syl2im ⊢ARB→BRC→ARB∧BRC→ARC
22 21 imp ⊢ARB∧BRC→ARB∧BRC→ARC
23 22 pm2.43i ⊢ARB∧BRC→ARC