sbcoteq1a

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

		Ref	Expression
	Assertion	sbcoteq1a	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ 𝜑 ) )

Proof

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

Metamath Proof Explorer

Theorem sbcoteq1a

Proof