Theorem opth 4554

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 4553	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4547	. . . . . . 7 |- { A } e. <. A , B >.
5		id 22	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2519	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 4072	. . . . . 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 460	. . . 4 |- ( <. A , B >. = <. C , D >. -> D e. _V )
10	3	opeq1d 4053	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2467	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 456	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 4045	. . . . . . . 8 |- ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14	12, 2, 13	sylancl 655	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15	11, 14	eqtr3d 2467	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 4045	. . . . . . 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 2467	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prex 4522	. . . . . 6 |- { C , B } e. _V
20		prex 4522	. . . . . 6 |- { C , D } e. _V
21	19, 20	preqr2 4035	. . . . 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 3943	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
24	23	eqeq2d 2444	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25		eqeq2 2442	. . . . . 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 2965	. . . . . 6 |- x e. _V
28	2, 27	preqr2 4035	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
29	26, 28	vtoclg 3019	. . . 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 529	. 2 |- ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
32		opeq12 4049	. 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 1362   e. wcel 1755   _Vcvv 2962   {csn 3865   {cpr 3867   <.cop 3871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872

This theorem is referenced by:  opthg  4555  otth2  4561  copsexg  4564  copsexgOLD  4565  copsex4g  4568  opcom  4573  moop2  4574  opelopabsbOLD  4586  ralxpf  4973  cnvcnvsn  5304  funopg  5438  xpopth  6604  eqop  6605  opiota  6622  soxp  6674  fnwelem  6676  xpdom2  7394  xpf1o  7461  unxpdomlem2  7506  unxpdomlem3  7507  xpwdomg  7788  fseqenlem1  8182  iundom2g  8692  eqresr  9292  cnref1o  10974  hashfun  12183  fsumcom2  13225  xpnnenOLD  13475  qredeu  13776  qnumdenbi  13805  crt  13836  prmreclem3  13962  imasaddfnlem  14449  dprd2da  16515  dprd2d2  16517  ucnima  19698  br8d  25766  xppreima2  25789  ofpreima  25808  erdszelem9  26935  fprodcom2  27342  brtp  27406  br8  27413  br6  27414  br4  27415  brsegle  27986  f1opr  28462  pellexlem3  29017  pellex  29021  oprabv  30003  numclwlk1lem2f1  30533  opelopab4  30961  dib1dim  34383  diclspsn  34412  dihopelvalcpre  34466  dihmeetlem4preN  34524  dihmeetlem13N  34537  dih1dimatlem  34547  dihatlat  34552