Theorem opeq2 3753

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 2227	. . . . . 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 2165	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3648	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3655	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2234	. . . . 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 969	. . . 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 969	. . . 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 2282	. 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 3579	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3579	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2222	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 967   = wceq 1342   e. wcel 2135   {cab 2150   _Vcvv 2721   {csn 3570   {cpr 3571   <.cop 3573

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579

This theorem is referenced by:  opeq12  3754  opeq2i  3756  opeq2d  3759  oteq2  3762  oteq3  3763  breq2  3980  cbvopab2  4050  cbvopab2v  4053  opthg  4210  eqvinop  4215  opelopabsb  4232  opelxp  4628  opabid2  4729  elrn2g  4788  opeldm  4801  opeldmg  4803  elrn2  4840  opelresg  4885  iss  4924  elimasng  4966  issref  4980  dmsnopg  5069  cnvsng  5083  elxp4  5085  elxp5  5086  dffun5r  5194  funopg  5216  f1osng  5467  tz6.12f  5509  fsn  5651  fsng  5652  fvsng  5675  oveq2  5844  cbvoprab2  5906  ovg  5971  opabex3d  6081  opabex3  6082  op1stg  6110  op2ndg  6111  oprssdmm  6131  op1steq  6139  dfoprab4f  6153  tfrlemibxssdm  6286  tfr1onlembxssdm  6302  tfrcllembxssdm  6315  elixpsn  6692  ixpsnf1o  6693  mapsnen  6768  xpsnen  6778  xpassen  6787  xpf1o  6801  djulclr  7005  djurclr  7006  djulcl  7007  djurcl  7008  djulclb  7011  inl11  7021  djuss  7026  1stinl  7030  2ndinl  7031  1stinr  7032  2ndinr  7033  elreal  7760  ax1rid  7809  fseq1p1m1  10019  cnmpt21  12832  djucllem  13516