Theorem opeq2 3884

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 2295	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 464	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2233	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3769	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3776	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2302	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 473	. . . 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 1007	. . . 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 1007	. . . 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 223	. . 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 2352	. 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 3698	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3698	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2290	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005   = wceq 1398   e. wcel 2203   {cab 2218   _Vcvv 2813   {csn 3689   {cpr 3690   <.cop 3692

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698

This theorem is referenced by:  opeq12  3885  opeq2i  3887  opeq2d  3890  oteq2  3893  oteq3  3894  breq2  4113  cbvopab2  4184  cbvopab2v  4187  opthg  4354  eqvinop  4359  opelopabsb  4378  opelxp  4779  opabid2  4886  elrn2g  4945  opeldm  4959  opeldmg  4961  elrn2  4999  opelresg  5045  iss  5084  elimasng  5130  issref  5145  dmsnopg  5234  cnvsng  5248  elxp4  5250  elxp5  5251  dffun5r  5364  funopg  5386  f1osng  5657  tz6.12f  5699  fsn  5849  fsng  5850  fvsng  5880  oveq2  6058  cbvoprab2  6126  ovg  6193  opabex3d  6314  opabex3  6315  op1stg  6344  op2ndg  6345  oprssdmm  6365  op1steq  6373  dfoprab4f  6387  elmpom  6434  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  elixpsn  6970  ixpsnf1o  6971  mapsnend  7052  mapsnen  7053  xpsnen  7072  xpassen  7081  xpf1o  7097  djulclr  7340  djurclr  7341  djulcl  7342  djurcl  7343  djulclb  7346  inl11  7356  djuss  7361  1stinl  7365  2ndinl  7366  1stinr  7367  2ndinr  7368  elreal  8143  ax1rid  8192  fseq1p1m1  10428  pfxval  11366  swrdccatin1  11417  swrdccat3blem  11431  imasaddfnlemg  13527  cnmpt21  15156  djucllem  16572