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 ⊢ x R y ∧ y R z → x R z
Assertion vtoclr ⊢ A R B ∧ B R C → A R C

Proof

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