Theorem opth 4714

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 4713	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4707	. . . . . . 7 |- { A } e. <. A , B >.
5		id 22	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2554	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 4231	. . . . . 6 |- ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
8	6, 7	syl 16	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
9	8	simprd 463	. . . 4 |- ( <. A , B >. = <. C , D >. -> D e. _V )
10	3	opeq1d 4212	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2503	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 459	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 4204	. . . . . . . 8 |- ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14	12, 2, 13	sylancl 662	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15	11, 14	eqtr3d 2503	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 4204	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
17	8, 16	syl 16	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
18	15, 17	eqtr3d 2503	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prex 4682	. . . . . 6 |- { C , B } e. _V
20		prex 4682	. . . . . 6 |- { C , D } e. _V
21	19, 20	preqr2 4194	. . . . 5 |- ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } )
22	18, 21	syl 16	. . . 4 |- ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )
23		preq2 4100	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
24	23	eqeq2d 2474	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25		eqeq2 2475	. . . . . 6 |- ( x = D -> ( B = x <-> B = D ) )
26	24, 25	imbi12d 320	. . . . 5 |- ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )
27		vex 3109	. . . . . 6 |- x e. _V
28	2, 27	preqr2 4194	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
29	26, 28	vtoclg 3164	. . . 4 |- ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )
30	9, 22, 29	sylc 60	. . 3 |- ( <. A , B >. = <. C , D >. -> B = D )
31	3, 30	jca 532	. 2 |- ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
32		opeq12 4208	. 2 |- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
33	31, 32	impbii 188	1 |- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   e. wcel 1762   _Vcvv 3106   {csn 4020   {cpr 4022   <.cop 4026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027

This theorem is referenced by:  opthg  4715  otth2  4721  copsexg  4725  copsexgOLD  4726  copsex4g  4729  opcom  4734  moop2  4735  opelopabsbALT  4749  ralxpf  5140  cnvcnvsn  5476  funopg  5611  oprabv  6320  xpopth  6813  eqop  6814  opiota  6833  soxp  6886  fnwelem  6888  xpdom2  7602  xpf1o  7669  unxpdomlem2  7715  unxpdomlem3  7716  xpwdomg  8000  fseqenlem1  8394  iundom2g  8904  eqresr  9503  cnref1o  11204  hashfun  12448  fsumcom2  13538  xpnnenOLD  13793  qredeu  14096  qnumdenbi  14125  crt  14156  prmreclem3  14284  imasaddfnlem  14772  dprd2da  16874  dprd2d2  16876  ucnima  20512  br8d  26986  xppreima2  27010  ofpreima  27029  erdszelem9  28133  fprodcom2  28541  brtp  28605  br8  28612  br6  28613  br4  28614  brsegle  29185  f1opr  29669  pellexlem3  30222  pellex  30226  numclwlk1lem2f1  31813  opelopab4  32279  dib1dim  35837  diclspsn  35866  dihopelvalcpre  35920  dihmeetlem4preN  35978  dihmeetlem13N  35991  dih1dimatlem  36001  dihatlat  36006