Metamath Proof Explorer


Theorem eqvinop

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of Monk2 p. 109. (Contributed by NM, 28-May-1995)

Ref Expression
Hypotheses eqvinop.1 B V
eqvinop.2 C V
Assertion eqvinop A = B C x y A = x y x y = B C

Proof

Step Hyp Ref Expression
1 eqvinop.1 B V
2 eqvinop.2 C V
3 1 2 opth2 x y = B C x = B y = C
4 3 anbi2i A = x y x y = B C A = x y x = B y = C
5 ancom A = x y x = B y = C x = B y = C A = x y
6 anass x = B y = C A = x y x = B y = C A = x y
7 4 5 6 3bitri A = x y x y = B C x = B y = C A = x y
8 7 exbii y A = x y x y = B C y x = B y = C A = x y
9 19.42v y x = B y = C A = x y x = B y y = C A = x y
10 opeq2 y = C x y = x C
11 10 eqeq2d y = C A = x y A = x C
12 2 11 ceqsexv y y = C A = x y A = x C
13 12 anbi2i x = B y y = C A = x y x = B A = x C
14 8 9 13 3bitri y A = x y x y = B C x = B A = x C
15 14 exbii x y A = x y x y = B C x x = B A = x C
16 opeq1 x = B x C = B C
17 16 eqeq2d x = B A = x C A = B C
18 1 17 ceqsexv x x = B A = x C A = B C
19 15 18 bitr2i A = B C x y A = x y x y = B C