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 ⊢ A = x y → ⦋ 1 st ⁡ A / x⦌ ⦋ 2 nd ⁡ A / y⦌ B = B

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 vex ⊢ y ∈ V
3 1 2 op2ndd ⊢ A = x y → 2 nd ⁡ A = y
4 3 eqcomd ⊢ A = x y → y = 2 nd ⁡ A
5 csbeq1a ⊢ y = 2 nd ⁡ A → B = ⦋ 2 nd ⁡ A / y⦌ B
6 4 5 syl ⊢ A = x y → B = ⦋ 2 nd ⁡ A / y⦌ B
7 1 2 op1std ⊢ A = x y → 1 st ⁡ A = x
8 7 eqcomd ⊢ A = x y → x = 1 st ⁡ A
9 csbeq1a ⊢ x = 1 st ⁡ A → ⦋ 2 nd ⁡ A / y⦌ B = ⦋ 1 st ⁡ A / x⦌ ⦋ 2 nd ⁡ A / y⦌ B
10 8 9 syl ⊢ A = x y → ⦋ 2 nd ⁡ A / y⦌ B = ⦋ 1 st ⁡ A / x⦌ ⦋ 2 nd ⁡ A / y⦌ B
11 6 10 eqtr2d ⊢ A = x y → ⦋ 1 st ⁡ A / x⦌ ⦋ 2 nd ⁡ A / y⦌ B = B