Theorem opeq2 3809

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 2259	. . . . . 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 2197	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3700	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3707	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2266	. . . . 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 982	. . . 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 982	. . . 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 2314	. 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 3631	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3631	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2254	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   = wceq 1364   e. wcel 2167   {cab 2182   _Vcvv 2763   {csn 3622   {cpr 3623   <.cop 3625

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631

This theorem is referenced by:  opeq12  3810  opeq2i  3812  opeq2d  3815  oteq2  3818  oteq3  3819  breq2  4037  cbvopab2  4107  cbvopab2v  4110  opthg  4271  eqvinop  4276  opelopabsb  4294  opelxp  4693  opabid2  4797  elrn2g  4856  opeldm  4869  opeldmg  4871  elrn2  4908  opelresg  4953  iss  4992  elimasng  5037  issref  5052  dmsnopg  5141  cnvsng  5155  elxp4  5157  elxp5  5158  dffun5r  5270  funopg  5292  f1osng  5545  tz6.12f  5587  fsn  5734  fsng  5735  fvsng  5758  oveq2  5930  cbvoprab2  5995  ovg  6062  opabex3d  6178  opabex3  6179  op1stg  6208  op2ndg  6209  oprssdmm  6229  op1steq  6237  dfoprab4f  6251  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  elixpsn  6794  ixpsnf1o  6795  mapsnen  6870  xpsnen  6880  xpassen  6889  xpf1o  6905  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djulclb  7121  inl11  7131  djuss  7136  1stinl  7140  2ndinl  7141  1stinr  7142  2ndinr  7143  elreal  7895  ax1rid  7944  fseq1p1m1  10169  imasaddfnlemg  12957  cnmpt21  14527  djucllem  15446