Theorem opth 4238

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 4237	. . 3 |- ( <. A , B >. = <. C , D >. -> A = C )
4	1, 2	opi1 4233	. . . . . . 7 |- { A } e. <. A , B >.
5		id 19	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , D >. )
6	4, 5	eleqtrid 2266	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { A } e. <. C , D >. )
7		oprcl 3803	. . . . . 6 |- ( { A } e. <. C , D >. -> ( C e. _V /\ D e. _V ) )
8	6, 7	syl 14	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( C e. _V /\ D e. _V ) )
9	8	simprd 114	. . . 4 |- ( <. A , B >. = <. C , D >. -> D e. _V )
10	3	opeq1d 3785	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> <. A , B >. = <. C , B >. )
11	10, 5	eqtr3d 2212	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = <. C , D >. )
12	8	simpld 112	. . . . . . . 8 |- ( <. A , B >. = <. C , D >. -> C e. _V )
13		dfopg 3777	. . . . . . . 8 |- ( ( C e. _V /\ B e. _V ) -> <. C , B >. = { { C } , { C , B } } )
14	12, 2, 13	sylancl 413	. . . . . . 7 |- ( <. A , B >. = <. C , D >. -> <. C , B >. = { { C } , { C , B } } )
15	11, 14	eqtr3d 2212	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , B } } )
16		dfopg 3777	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> <. C , D >. = { { C } , { C , D } } )
17	8, 16	syl 14	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> <. C , D >. = { { C } , { C , D } } )
18	15, 17	eqtr3d 2212	. . . . 5 |- ( <. A , B >. = <. C , D >. -> { { C } , { C , B } } = { { C } , { C , D } } )
19		prexg 4212	. . . . . . 7 |- ( ( C e. _V /\ B e. _V ) -> { C , B } e. _V )
20	12, 2, 19	sylancl 413	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { C , B } e. _V )
21		prexg 4212	. . . . . . 7 |- ( ( C e. _V /\ D e. _V ) -> { C , D } e. _V )
22	8, 21	syl 14	. . . . . 6 |- ( <. A , B >. = <. C , D >. -> { C , D } e. _V )
23		preqr2g 3768	. . . . . 6 |- ( ( { C , B } e. _V /\ { C , D } e. _V ) -> ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } ) )
24	20, 22, 23	syl2anc 411	. . . . 5 |- ( <. A , B >. = <. C , D >. -> ( { { C } , { C , B } } = { { C } , { C , D } } -> { C , B } = { C , D } ) )
25	18, 24	mpd 13	. . . 4 |- ( <. A , B >. = <. C , D >. -> { C , B } = { C , D } )
26		preq2 3671	. . . . . . 7 |- ( x = D -> { C , x } = { C , D } )
27	26	eqeq2d 2189	. . . . . 6 |- ( x = D -> ( { C , B } = { C , x } <-> { C , B } = { C , D } ) )
28		eqeq2 2187	. . . . . 6 |- ( x = D -> ( B = x <-> B = D ) )
29	27, 28	imbi12d 234	. . . . 5 |- ( x = D -> ( ( { C , B } = { C , x } -> B = x ) <-> ( { C , B } = { C , D } -> B = D ) ) )
30		vex 2741	. . . . . 6 |- x e. _V
31	2, 30	preqr2 3770	. . . . 5 |- ( { C , B } = { C , x } -> B = x )
32	29, 31	vtoclg 2798	. . . 4 |- ( D e. _V -> ( { C , B } = { C , D } -> B = D ) )
33	9, 25, 32	sylc 62	. . 3 |- ( <. A , B >. = <. C , D >. -> B = D )
34	3, 33	jca 306	. 2 |- ( <. A , B >. = <. C , D >. -> ( A = C /\ B = D ) )
35		opeq12 3781	. 2 |- ( ( A = C /\ B = D ) -> <. A , B >. = <. C , D >. )
36	34, 35	impbii 126	1 |- ( <. A , B >. = <. C , D >. <-> ( A = C /\ B = D ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   e. wcel 2148   _Vcvv 2738   {csn 3593   {cpr 3594   <.cop 3596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602

This theorem is referenced by:  opthg  4239  otth2  4242  copsexg  4245  copsex4g  4248  opcom  4251  moop2  4252  opelopabsbALT  4260  opelopabsb  4261  ralxpf  4774  rexxpf  4775  cnvcnvsn  5106  funopg  5251  funinsn  5266  brabvv  5921  xpdom2  6831  xpf1o  6844  djuf1olem  7052  enq0ref  7432  enq0tr  7433  mulnnnq0  7449  eqresr  7835  cnref1o  9650  fisumcom2  11446  fprodcom2fi  11634  qredeu  12097  fnpr2ob  12759