Theorem opeq2 3653

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 2162	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 455	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2101	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3548	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3555	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2169	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 460	. . . 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 932	. . . 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 932	. . . 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 2217	. 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 3483	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3483	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2157	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 930   = wceq 1299   e. wcel 1448   {cab 2086   _Vcvv 2641   {csn 3474   {cpr 3475   <.cop 3477

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483

This theorem is referenced by:  opeq12  3654  opeq2i  3656  opeq2d  3659  oteq2  3662  oteq3  3663  breq2  3879  cbvopab2  3942  cbvopab2v  3945  opthg  4098  eqvinop  4103  opelopabsb  4120  opelxp  4507  opabid2  4608  elrn2g  4667  opeldm  4680  opeldmg  4682  elrn2  4719  opelresg  4762  iss  4801  elimasng  4843  issref  4857  dmsnopg  4946  cnvsng  4960  elxp4  4962  elxp5  4963  dffun5r  5071  funopg  5093  f1osng  5342  tz6.12f  5382  fsn  5524  fsng  5525  fvsng  5548  oveq2  5714  cbvoprab2  5776  ovg  5841  opabex3d  5950  opabex3  5951  op1stg  5979  op2ndg  5980  op1steq  6007  dfoprab4f  6021  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  elixpsn  6559  ixpsnf1o  6560  mapsnen  6635  xpsnen  6644  xpassen  6653  xpf1o  6667  djulclr  6849  djurclr  6850  djulcl  6851  djurcl  6852  djulclb  6855  inl11  6865  djuss  6870  1stinl  6874  2ndinl  6875  1stinr  6876  2ndinr  6877  elreal  7516  ax1rid  7562  fseq1p1m1  9715  cnmpt21  12241  djucllem  12588