Theorem opth 4679

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 4678	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4672	. . . . . . 7 |- { A } e. <. A , B >.
5		id 22	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2537	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 4194	. . . . . 6 |- ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
8	6, 7	syl 17	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
9	8	simprd 465	. . . 4 |- ( <. A , B >. = <. C , D >. -> D e. _V )
10	3	opeq1d 4175	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2489	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 461	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 4167	. . . . . . . 8 |- ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14	12, 2, 13	sylancl 669	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15	11, 14	eqtr3d 2489	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 4167	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
17	8, 16	syl 17	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
18	15, 17	eqtr3d 2489	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prex 4645	. . . . . 6 |- { C , B } e. _V
20		prex 4645	. . . . . 6 |- { C , D } e. _V
21	19, 20	preqr2 4153	. . . . 5 |- ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } )
22	18, 21	syl 17	. . . 4 |- ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )
23		preq2 4055	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
24	23	eqeq2d 2463	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25		eqeq2 2464	. . . . . 6 |- ( x = D -> ( B = x <-> B = D ) )
26	24, 25	imbi12d 322	. . . . 5 |- ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )
27		vex 3050	. . . . . 6 |- x e. _V
28	2, 27	preqr2 4153	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
29	26, 28	vtoclg 3109	. . . 4 |- ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )
30	9, 22, 29	sylc 62	. . 3 |- ( <. A , B >. = <. C , D >. -> B = D )
31	3, 30	jca 535	. 2 |- ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
32		opeq12 4171	. 2 |- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
33	31, 32	impbii 191	1 |- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1446   e. wcel 1889   _Vcvv 3047   {csn 3970   {cpr 3972   <.cop 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977

This theorem is referenced by:  opthg  4680  otth2  4686  copsexg  4690  copsex4g  4693  opcom  4698  moop2  4699  opelopabsbALT  4713  ralxpf  4984  cnvcnvsn  5316  funopg  5617  tpres  6122  oprabv  6344  xpopth  6837  eqop  6838  opiota  6857  soxp  6914  fnwelem  6916  xpdom2  7672  xpf1o  7739  unxpdomlem2  7782  unxpdomlem3  7783  xpwdomg  8105  fseqenlem1  8460  iundom2g  8970  eqresr  9566  cnref1o  11304  hashfun  12616  fsumcom2  13847  fprodcom2  14050  qredeu  14676  qnumdenbi  14705  crt  14738  prmreclem3  14874  imasaddfnlem  15446  dprd2da  17687  dprd2d2  17689  ucnima  21308  numclwlk1lem2f1  25834  br8d  28230  xppreima2  28261  aciunf1lem  28276  ofpreima  28280  erdszelem9  29934  msubff1  30206  mvhf1  30209  brtp  30401  br8  30408  br6  30409  br4  30410  brsegle  30887  poimirlem4  31956  poimirlem9  31961  f1opr  32063  dib1dim  34745  diclspsn  34774  dihopelvalcpre  34828  dihmeetlem4preN  34886  dihmeetlem13N  34899  dih1dimatlem  34909  dihatlat  34914  pellexlem3  35687  pellex  35691  snhesn  36394  opelopab4  36929  propssopi  39010  funsndifnop  39032