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

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
2		vex	⊢ 𝑧 ∈ V
3	1 2	op2ndd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2^nd ‘ 𝐴 ) = 𝑧 )
4	3	eqcomd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑧 = ( 2^nd ‘ 𝐴 ) )
5		sbceq1a	⊢ ( 𝑧 = ( 2^nd ‘ 𝐴 ) → ( 𝜑 ↔ [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
6	4 5	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8 2	ot22ndd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) = 𝑦 )
10	9	eqcomd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) )
11		sbceq1a	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) → ( [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
12	10 11	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
13	7 8 2	ot21std	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) = 𝑥 )
14	13	eqcomd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) )
15		sbceq1a	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) → ( [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
16	14 15	syl	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ) )
17	6 12 16	3bitrrd	⊢ ( 𝐴 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝐴 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝐴 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝐴 ) / 𝑧 ] 𝜑 ↔ 𝜑 ) )