Theorem opth 2863

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 is not required to be a set due to a peculiarity of our specific ordered pair definition.

Hypotheses

Ref	Expression
opth.1	|- A e. V
opth.2	|- B e. V
opth.3	|- D e. V

Assertion

Ref	Expression
opth	|- (<.A, B>. = <.C, D>. <-> (A = C /\ B = D))

Proof of Theorem opth

Step	Hyp	Ref	Expression
1		opth.1	. . . 4 |- A e. V
2	1	opth1 2862	. . 3 |- (<.A, B>. = <.C, D>. -> A = C)
3		eqeq1 1524	. . . . 5 |- (<.A, B>. = <.C, D>. -> (<.A, B>. = <.C, B>. <-> <.C, D>. = <.C, B>.))
4		opeq1 2552	. . . . 5 |- (A = C -> <.A, B>. = <.C, B>.)
5	3, 4	syl5bi 206	. . . 4 |- (<.A, B>. = <.C, D>. -> (A = C -> <.C, D>. = <.C, B>.))
6		df-op 2474	. . . . . . 7 |- <.C, D>. = {{C}, {C, D}}
7		df-op 2474	. . . . . . 7 |- <.C, B>. = {{C}, {C, B}}
8	6, 7	eqeq12i 1531	. . . . . 6 |- (<.C, D>. = <.C, B>. <-> {{C}, {C, D}} = {{C}, {C, B}})
9		prex 2857	. . . . . . 7 |- {C, D} e. V
10		prex 2857	. . . . . . 7 |- {C, B} e. V
11	9, 10	preqr2 2547	. . . . . 6 |- ({{C}, {C, D}} = {{C}, {C, B}} -> {C, D} = {C, B})
12	8, 11	sylbi 197	. . . . 5 |- (<.C, D>. = <.C, B>. -> {C, D} = {C, B})
13		opth.3	. . . . . . 7 |- D e. V
14		opth.2	. . . . . . 7 |- B e. V
15	13, 14	preqr2 2547	. . . . . 6 |- ({C, D} = {C, B} -> D = B)
16	15	eqcomd 1523	. . . . 5 |- ({C, D} = {C, B} -> B = D)
17	12, 16	syl 10	. . . 4 |- (<.C, D>. = <.C, B>. -> B = D)
18	5, 17	syl6 22	. . 3 |- (<.A, B>. = <.C, D>. -> (A = C -> B = D))
19	2, 18	jcai 287	. 2 |- (<.A, B>. = <.C, D>. -> (A = C /\ B = D))
20		opeq12 2554	. 2 |- ((A = C /\ B = D) -> <.A, B>. = <.C, D>.)
21	19, 20	impbii 155	1 |- (<.A, B>. = <.C, D>. <-> (A = C /\ B = D))

Syntax hints:   <-> wb 144   /\ wa 221   = wceq 992   e. wcel 994  Vcvv 1857  {csn 2467  {cpr 2468  <.cop 2469

This theorem is referenced by:  opthg 2864  eqvinop 2867  copsexg 2868  opth2 2876  opabid 2887  opelxp 3297  ralxpf 3303  cnvsn 3580  funopg 3652  iunfopab 3719  fsn 3948  xpopth 4166  xpdom2 4583  aceq5lem4 4884  unidom 4954  eqresr 5409  ltresr 5412  xpnnen 7711  ipfval 8606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474

Copyright terms: Public domain