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]˙ φ φ