This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) / 𝑦 ⦌ 𝐵 = 𝐵 )