Theorem opth 4664

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 4663	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4657	. . . . . . 7 |- { A } e. <. A , B >.
5		id 22	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2545	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 4182	. . . . . 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 4163	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2494	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 459	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 4155	. . . . . . . 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 2494	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 4155	. . . . . . 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 2494	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prex 4632	. . . . . 6 |- { C , B } e. _V
20		prex 4632	. . . . . 6 |- { C , D } e. _V
21	19, 20	preqr2 4145	. . . . 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 4053	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
24	23	eqeq2d 2465	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25		eqeq2 2466	. . . . . 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 3071	. . . . . 6 |- x e. _V
28	2, 27	preqr2 4145	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
29	26, 28	vtoclg 3126	. . . 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 4159	. 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 1370   e. wcel 1758   _Vcvv 3068   {csn 3975   {cpr 3977   <.cop 3981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982

This theorem is referenced by:  opthg  4665  otth2  4671  copsexg  4674  copsexgOLD  4675  copsex4g  4678  opcom  4683  moop2  4684  opelopabsbALT  4696  ralxpf  5084  cnvcnvsn  5414  funopg  5548  xpopth  6715  eqop  6716  opiota  6733  soxp  6785  fnwelem  6787  xpdom2  7506  xpf1o  7573  unxpdomlem2  7619  unxpdomlem3  7620  xpwdomg  7901  fseqenlem1  8295  iundom2g  8805  eqresr  9405  cnref1o  11087  hashfun  12301  fsumcom2  13343  xpnnenOLD  13594  qredeu  13895  qnumdenbi  13924  crt  13955  prmreclem3  14081  imasaddfnlem  14568  dprd2da  16646  dprd2d2  16648  ucnima  19972  br8d  26076  xppreima2  26099  ofpreima  26118  erdszelem9  27221  fprodcom2  27629  brtp  27693  br8  27700  br6  27701  br4  27702  brsegle  28273  f1opr  28756  pellexlem3  29310  pellex  29314  oprabv  30295  numclwlk1lem2f1  30825  opelopab4  31560  dib1dim  35116  diclspsn  35145  dihopelvalcpre  35199  dihmeetlem4preN  35257  dihmeetlem13N  35270  dih1dimatlem  35280  dihatlat  35285