Theorem opeq2 3889

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 2297	. . . . . 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 2235	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3774	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3781	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2304	. . . . 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 2354	. 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 3703	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3703	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2292	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005   = wceq 1398   e. wcel 2205   {cab 2220   _Vcvv 2815   {csn 3694   {cpr 3695   <.cop 3697

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703

This theorem is referenced by:  opeq12  3890  opeq2i  3892  opeq2d  3895  oteq2  3898  oteq3  3899  breq2  4118  cbvopab2  4189  cbvopab2v  4192  opthg  4359  eqvinop  4364  opelopabsb  4383  opelxp  4784  opabid2  4891  elrn2g  4950  opeldm  4964  opeldmg  4966  elrn2  5004  opelresg  5050  iss  5089  elimasng  5135  issref  5150  dmsnopg  5239  cnvsng  5253  elxp4  5255  elxp5  5256  dffun5r  5369  funopg  5391  f1osng  5662  tz6.12f  5704  fsn  5854  fsng  5855  fvsng  5885  oveq2  6066  cbvoprab2  6134  ovg  6201  opabex3d  6323  opabex3  6324  op1stg  6357  op2ndg  6358  oprssdmm  6378  op1steq  6386  dfoprab4f  6400  elmpom  6447  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  elixpsn  6983  ixpsnf1o  6984  mapsnend  7065  mapsnen  7066  xpsnen  7085  xpassen  7094  xpf1o  7110  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djulclb  7359  inl11  7369  djuss  7374  1stinl  7378  2ndinl  7379  1stinr  7380  2ndinr  7381  elreal  8159  ax1rid  8208  fseq1p1m1  10450  pfxval  11391  swrdccatin1  11442  swrdccat3blem  11456  imasaddfnlemg  13578  cnmpt21  15282  djucllem  16698