Theorem opth 3992

Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that C and D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)

Hypotheses

Ref	Expression
opth1.1	|- A e. _V
opth1.2	|- B e. _V

Assertion

Ref	Expression
opth	|- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Proof of Theorem opth

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opth1.1	. . . 4 |- A e. _V
2		opth1.2	. . . 4 |- B e. _V
3	1, 2	opth1 3991	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 3987	. . . . . . 7 |- { A } e. <. A , B >.
5		id 19	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2167	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 3594	. . . . . 6 |- ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
8	6, 7	syl 14	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
9	8	simprd 112	. . . 4 |- ( <. A , B >. = <. C , D >. -> D e. _V )
10	3	opeq1d 3576	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2115	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 110	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 3568	. . . . . . . 8 |- ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14	12, 2, 13	sylancl 404	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15	11, 14	eqtr3d 2115	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 3568	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
17	8, 16	syl 14	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
18	15, 17	eqtr3d 2115	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prexg 3966	. . . . . . 7 |- ( ( C e. _V /\ B e. _V ) -> { C , B } e. _V )
20	12, 2, 19	sylancl 404	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { C , B } e. _V )
21		prexg 3966	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> { C , D } e. _V )
22	8, 21	syl 14	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { C , D } e. _V )
23		preqr2g 3559	. . . . . 6 |- ( ( { C , B } e. _V /\ { C , D } e. _V ) -> ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } ) )
24	20, 22, 23	syl2anc 403	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } ) )
25	18, 24	mpd 13	. . . 4 |- ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )
26		preq2 3470	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
27	26	eqeq2d 2092	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
28		eqeq2 2090	. . . . . 6 |- ( x = D -> ( B = x <-> B = D ) )
29	27, 28	imbi12d 232	. . . . 5 |- ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )
30		vex 2604	. . . . . 6 |- x e. _V
31	2, 30	preqr2 3561	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
32	29, 31	vtoclg 2658	. . . 4 |- ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )
33	9, 25, 32	sylc 61	. . 3 |- ( <. A , B >. = <. C , D >. -> B = D )
34	3, 33	jca 300	. 2 |- ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
35		opeq12 3572	. 2 |- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
36	34, 35	impbii 124	1 |- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   e. wcel 1433   _Vcvv 2601   {csn 3398   {cpr 3399   <.cop 3401

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407

This theorem is referenced by:  opthg  3993  otth2  3996  copsexg  3999  copsex4g  4002  opcom  4005  moop2  4006  opelopabsbALT  4014  opelopabsb  4015  ralxpf  4500  rexxpf  4501  cnvcnvsn  4817  funopg  4954  brabvv  5571  xpdom2  6328  enq0ref  6623  enq0tr  6624  mulnnnq0  6640  eqresr  7004  cnref1o  8733  qredeu  10479