Theorem opth 4561

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 4560	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4554	. . . . . . 7 |- { A } e. <. A , B >.
5		id 22	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	syl5eleq 2524	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 4079	. . . . . 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 4060	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2472	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 459	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 4052	. . . . . . . 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 2472	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 4052	. . . . . . 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 2472	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prex 4529	. . . . . 6 |- { C , B } e. _V
20		prex 4529	. . . . . 6 |- { C , D } e. _V
21	19, 20	preqr2 4042	. . . . 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 3950	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
24	23	eqeq2d 2449	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
25		eqeq2 2447	. . . . . 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 2970	. . . . . 6 |- x e. _V
28	2, 27	preqr2 4042	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
29	26, 28	vtoclg 3025	. . . 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 4056	. 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 1369   e. wcel 1756   _Vcvv 2967   {csn 3872   {cpr 3874   <.cop 3878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879

This theorem is referenced by:  opthg  4562  otth2  4568  copsexg  4571  copsexgOLD  4572  copsex4g  4575  opcom  4580  moop2  4581  opelopabsbALT  4593  ralxpf  4981  cnvcnvsn  5311  funopg  5445  xpopth  6610  eqop  6611  opiota  6628  soxp  6680  fnwelem  6682  xpdom2  7398  xpf1o  7465  unxpdomlem2  7510  unxpdomlem3  7511  xpwdomg  7792  fseqenlem1  8186  iundom2g  8696  eqresr  9296  cnref1o  10978  hashfun  12191  fsumcom2  13233  xpnnenOLD  13484  qredeu  13785  qnumdenbi  13814  crt  13845  prmreclem3  13971  imasaddfnlem  14458  dprd2da  16531  dprd2d2  16533  ucnima  19836  br8d  25910  xppreima2  25933  ofpreima  25952  erdszelem9  27056  fprodcom2  27464  brtp  27528  br8  27535  br6  27536  br4  27537  brsegle  28108  f1opr  28589  pellexlem3  29143  pellex  29147  oprabv  30128  numclwlk1lem2f1  30658  opelopab4  31189  dib1dim  34703  diclspsn  34732  dihopelvalcpre  34786  dihmeetlem4preN  34844  dihmeetlem13N  34857  dih1dimatlem  34867  dihatlat  34872