Theorem eqvinop 2797

Description: A variable introduction law for ordered pairs. Analogue of Lemma 15 of [Monk2] p. 109.

Hypotheses

Ref	Expression
eqvinop.1	|- B e. V
eqvinop.2	|- C e. V

Assertion

Ref	Expression
eqvinop	|- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))

Distinct variable groups:   x,y,A   x,B,y   x,C,y

Proof of Theorem eqvinop

Step	Hyp	Ref	Expression
1		visset 1816	. . . . . . . 8 |- x e. V
2		visset 1816	. . . . . . . 8 |- y e. V
3		eqvinop.2	. . . . . . . 8 |- C e. V
4	1, 2, 3	opth 2793	. . . . . . 7 |- (<.x, y>. = <.B, C>. <-> (x = B /\ y = C))
5	4	anbi2i 482	. . . . . 6 |- ((A = <.x, y>. /\ <.x, y>. = <.B, C>.) <-> (A = <.x, y>. /\ (x = B /\ y = C)))
6		ancom 437	. . . . . 6 |- ((A = <.x, y>. /\ (x = B /\ y = C)) <-> ((x = B /\ y = C) /\ A = <.x, y>.))
7		anass 441	. . . . . 6 |- (((x = B /\ y = C) /\ A = <.x, y>.) <-> (x = B /\ (y = C /\ A = <.x, y>.)))
8	5, 6, 7	3bitr 177	. . . . 5 |- ((A = <.x, y>. /\ <.x, y>. = <.B, C>.) <-> (x = B /\ (y = C /\ A = <.x, y>.)))
9	8	exbii 1053	. . . 4 |- (E.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.) <-> E.y(x = B /\ (y = C /\ A = <.x, y>.)))
10		19.42v 1310	. . . 4 |- (E.y(x = B /\ (y = C /\ A = <.x, y>.)) <-> (x = B /\ E.y(y = C /\ A = <.x, y>.)))
11		opeq2 2492	. . . . . . 7 |- (y = C -> <.x, y>. = <.x, C>.)
12	11	eqeq2d 1489	. . . . . 6 |- (y = C -> (A = <.x, y>. <-> A = <.x, C>.))
13	3, 12	ceqsexv 1838	. . . . 5 |- (E.y(y = C /\ A = <.x, y>.) <-> A = <.x, C>.)
14	13	anbi2i 482	. . . 4 |- ((x = B /\ E.y(y = C /\ A = <.x, y>.)) <-> (x = B /\ A = <.x, C>.))
15	9, 10, 14	3bitr 177	. . 3 |- (E.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.) <-> (x = B /\ A = <.x, C>.))
16	15	exbii 1053	. 2 |- (E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.) <-> E.x(x = B /\ A = <.x, C>.))
17		eqvinop.1	. . 3 |- B e. V
18		opeq1 2491	. . . 4 |- (x = B -> <.x, C>. = <.B, C>.)
19	18	eqeq2d 1489	. . 3 |- (x = B -> (A = <.x, C>. <-> A = <.B, C>.))
20	17, 19	ceqsexv 1838	. 2 |- (E.x(x = B /\ A = <.x, C>.) <-> A = <.B, C>.)
21	16, 20	bitr2 174	1 |- (A = <.B, C>. <-> E.xE.y(A = <.x, y>. /\ <.x, y>. = <.B, C>.))

Syntax hints:   <-> wb 146   /\ wa 223   = wceq 958   e. wcel 960  E.wex 982  Vcvv 1814  <.cop 2415

This theorem is referenced by:  copsexg 2798  ralxpf 3226

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-pow 2748  ax-pr 2785

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420

Copyright terms: Public domain