Theorem opeq2 3759

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	|- ( A = B -> <. C , A >. = <. C , B >. )

Proof of Theorem opeq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2229	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 460	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2166	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3654	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3661	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2236	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 465	. . . 4 |- ( A = B -> ( ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) ) )
8		df-3an 970	. . . 4 |- ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) )
9		df-3an 970	. . . 4 |- ( ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) )
10	7, 8, 9	3bitr4g 222	. . 3 |- ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) )
11	10	abbidv 2284	. 2 |- ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } )
12		df-op 3585	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3585	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2224	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 968   = wceq 1343   e. wcel 2136   {cab 2151   _Vcvv 2726   {csn 3576   {cpr 3577   <.cop 3579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585

This theorem is referenced by:  opeq12  3760  opeq2i  3762  opeq2d  3765  oteq2  3768  oteq3  3769  breq2  3986  cbvopab2  4056  cbvopab2v  4059  opthg  4216  eqvinop  4221  opelopabsb  4238  opelxp  4634  opabid2  4735  elrn2g  4794  opeldm  4807  opeldmg  4809  elrn2  4846  opelresg  4891  iss  4930  elimasng  4972  issref  4986  dmsnopg  5075  cnvsng  5089  elxp4  5091  elxp5  5092  dffun5r  5200  funopg  5222  f1osng  5473  tz6.12f  5515  fsn  5657  fsng  5658  fvsng  5681  oveq2  5850  cbvoprab2  5915  ovg  5980  opabex3d  6089  opabex3  6090  op1stg  6118  op2ndg  6119  oprssdmm  6139  op1steq  6147  dfoprab4f  6161  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  elixpsn  6701  ixpsnf1o  6702  mapsnen  6777  xpsnen  6787  xpassen  6796  xpf1o  6810  djulclr  7014  djurclr  7015  djulcl  7016  djurcl  7017  djulclb  7020  inl11  7030  djuss  7035  1stinl  7039  2ndinl  7040  1stinr  7041  2ndinr  7042  elreal  7769  ax1rid  7818  fseq1p1m1  10029  cnmpt21  12931  djucllem  13681