Theorem opeq2 3834

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 2270	. . . . . 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 2208	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3721	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3728	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2277	. . . . 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 983	. . . 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 983	. . . 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 2325	. 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 3652	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3652	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2265	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   = wceq 1373   e. wcel 2178   {cab 2193   _Vcvv 2776   {csn 3643   {cpr 3644   <.cop 3646

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  opeq12  3835  opeq2i  3837  opeq2d  3840  oteq2  3843  oteq3  3844  breq2  4063  cbvopab2  4134  cbvopab2v  4137  opthg  4300  eqvinop  4305  opelopabsb  4324  opelxp  4723  opabid2  4827  elrn2g  4886  opeldm  4900  opeldmg  4902  elrn2  4939  opelresg  4985  iss  5024  elimasng  5069  issref  5084  dmsnopg  5173  cnvsng  5187  elxp4  5189  elxp5  5190  dffun5r  5302  funopg  5324  f1osng  5586  tz6.12f  5628  fsn  5775  fsng  5776  fvsng  5803  oveq2  5975  cbvoprab2  6041  ovg  6108  opabex3d  6229  opabex3  6230  op1stg  6259  op2ndg  6260  oprssdmm  6280  op1steq  6288  dfoprab4f  6302  tfrlemibxssdm  6436  tfr1onlembxssdm  6452  tfrcllembxssdm  6465  elixpsn  6845  ixpsnf1o  6846  mapsnen  6927  xpsnen  6941  xpassen  6950  xpf1o  6966  djulclr  7177  djurclr  7178  djulcl  7179  djurcl  7180  djulclb  7183  inl11  7193  djuss  7198  1stinl  7202  2ndinl  7203  1stinr  7204  2ndinr  7205  elreal  7976  ax1rid  8025  fseq1p1m1  10251  pfxval  11165  swrdccatin1  11216  swrdccat3blem  11230  imasaddfnlemg  13261  cnmpt21  14878  djucllem  15936