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 fveq2 A = x y z 2 nd A = 2 nd x y z
2 ot3rdg z V 2 nd x y z = z
3 2 elv 2 nd x y z = z
4 1 3 eqtr2di 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 2fveq3 A = x y z 2 nd 1 st A = 2 nd 1 st x y z
8 vex x V
9 vex y V
10 vex z V
11 ot2ndg x V y V z V 2 nd 1 st x y z = y
12 8 9 10 11 mp3an 2 nd 1 st x y z = y
13 7 12 eqtr2di A = x y z y = 2 nd 1 st A
14 sbceq1a y = 2 nd 1 st A [˙ 2 nd A / z]˙ φ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
15 13 14 syl A = x y z [˙ 2 nd A / z]˙ φ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ
16 2fveq3 A = x y z 1 st 1 st A = 1 st 1 st x y z
17 ot1stg x V y V z V 1 st 1 st x y z = x
18 8 9 10 17 mp3an 1 st 1 st x y z = x
19 16 18 eqtr2di A = x y z x = 1 st 1 st A
20 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]˙ φ
21 19 20 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]˙ φ
22 6 15 21 3bitrrd A = x y z [˙ 1 st 1 st A / x]˙ [˙ 2 nd 1 st A / y]˙ [˙ 2 nd A / z]˙ φ φ