Theorem csbopeq1a

Description: Equality theorem for substitution of a class A for an ordered pair <. x , y >. in B (analogue of csbeq1a ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	csbopeq1a	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 1st ‘ 𝐴 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	op2ndd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝐴 ) = 𝑦 )
4	3	eqcomd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ( 2nd ‘ 𝐴 ) )
5		csbeq1a	⊢ ( 𝑦 = ( 2nd ‘ 𝐴 ) → 𝐵 = ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 )
6	4 5	syl	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐵 = ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 )
7	1 2	op1std	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1st ‘ 𝐴 ) = 𝑥 )
8	7	eqcomd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑥 = ( 1st ‘ 𝐴 ) )
9		csbeq1a	⊢ ( 𝑥 = ( 1st ‘ 𝐴 ) → ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 = ⦋ ( 1st ‘ 𝐴 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 )
10	8 9	syl	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 = ⦋ ( 1st ‘ 𝐴 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 )
11	6 10	eqtr2d	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 1st ‘ 𝐴 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 = 𝐵 )