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

Metamath Proof Explorer

Theorem sbcopeq1a

Description: Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a that avoids the existential quantifiers of copsexg ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion sbcopeq1a ⊢ A = x y → [˙ 1 st ⁡ A / x]˙ [˙ 2 nd ⁡ A / y]˙ φ ↔ φ

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 sbceq1a ⊢ y = 2 nd ⁡ A → φ ↔ [˙ 2 nd ⁡ A / y]˙ φ
6 4 5 syl ⊢ A = x y → φ ↔ [˙ 2 nd ⁡ A / y]˙ φ
7 1 2 op1std ⊢ A = x y → 1 st ⁡ A = x
8 7 eqcomd ⊢ A = x y → x = 1 st ⁡ A
9 sbceq1a ⊢ x = 1 st ⁡ A → [˙ 2 nd ⁡ A / y]˙ φ ↔ [˙ 1 st ⁡ A / x]˙ [˙ 2 nd ⁡ A / y]˙ φ
10 8 9 syl ⊢ A = x y → [˙ 2 nd ⁡ A / y]˙ φ ↔ [˙ 1 st ⁡ A / x]˙ [˙ 2 nd ⁡ A / y]˙ φ
11 6 10 bitr2d ⊢ A = x y → [˙ 1 st ⁡ A / x]˙ [˙ 2 nd ⁡ A / y]˙ φ ↔ φ