Metamath Proof Explorer


Theorem sbcoteq1a

Description: Equality theorem for substitution of a class for an ordered triple. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Assertion sbcoteq1a A = x y z [˙ 1 st 1 st A / x]˙ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ φ

Proof

Step Hyp Ref Expression
1 opex x y V
2 vex z V
3 1 2 op2ndd A = x y z 2 nd A = z
4 3 eqcomd A = x y z z = 2 nd A
5 sbceq1a z = 2 nd A φ [˙ 2 nd A / z]˙ φ
6 4 5 syl A = x y z φ [˙ 2 nd A / z]˙ φ
7 vex x V
8 vex y V
9 7 8 2 ot22ndd A = x y z 2 nd 1 st A = y
10 9 eqcomd A = x y z y = 2 nd 1 st A
11 sbceq1a y = 2 nd 1 st A [˙ 2 nd A / z]˙ φ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
12 10 11 syl A = x y z [˙ 2 nd A / z]˙ φ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
13 7 8 2 ot21std A = x y z 1 st 1 st A = x
14 13 eqcomd A = x y z x = 1 st 1 st A
15 sbceq1a x = 1 st 1 st A [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ [˙ 1 st 1 st A / x]˙ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
16 14 15 syl A = x y z [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ [˙ 1 st 1 st A / x]˙ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
17 6 12 16 3bitrrd A = x y z [˙ 1 st 1 st A / x]˙ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ φ