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 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( [ ( 1st ‘ ( 1st𝐴 ) ) / 𝑥 ] [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑𝜑 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 2nd𝐴 ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
2 ot3rdg ( 𝑧 ∈ V → ( 2nd ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) = 𝑧 )
3 2 elv ( 2nd ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) = 𝑧
4 1 3 eqtr2di ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝑧 = ( 2nd𝐴 ) )
5 sbceq1a ( 𝑧 = ( 2nd𝐴 ) → ( 𝜑[ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
6 4 5 syl ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 𝜑[ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
7 2fveq3 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 2nd ‘ ( 1st𝐴 ) ) = ( 2nd ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
8 vex 𝑥 ∈ V
9 vex 𝑦 ∈ V
10 vex 𝑧 ∈ V
11 ot2ndg ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 2nd ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = 𝑦 )
12 8 9 10 11 mp3an ( 2nd ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = 𝑦
13 7 12 eqtr2di ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝑦 = ( 2nd ‘ ( 1st𝐴 ) ) )
14 sbceq1a ( 𝑦 = ( 2nd ‘ ( 1st𝐴 ) ) → ( [ ( 2nd𝐴 ) / 𝑧 ] 𝜑[ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
15 13 14 syl ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( [ ( 2nd𝐴 ) / 𝑧 ] 𝜑[ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
16 2fveq3 ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( 1st ‘ ( 1st𝐴 ) ) = ( 1st ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
17 ot1stg ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 1st ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = 𝑥 )
18 8 9 10 17 mp3an ( 1st ‘ ( 1st ‘ ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = 𝑥
19 16 18 eqtr2di ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → 𝑥 = ( 1st ‘ ( 1st𝐴 ) ) )
20 sbceq1a ( 𝑥 = ( 1st ‘ ( 1st𝐴 ) ) → ( [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑[ ( 1st ‘ ( 1st𝐴 ) ) / 𝑥 ] [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
21 19 20 syl ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑[ ( 1st ‘ ( 1st𝐴 ) ) / 𝑥 ] [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑 ) )
22 6 15 21 3bitrrd ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( [ ( 1st ‘ ( 1st𝐴 ) ) / 𝑥 ] [ ( 2nd ‘ ( 1st𝐴 ) ) / 𝑦 ] [ ( 2nd𝐴 ) / 𝑧 ] 𝜑𝜑 ) )