Theorem opeq2 3805

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 2256	. . . . . 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 2194	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3696	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3703	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2263	. . . . 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 2311	. 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 3627	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3627	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2251	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   = wceq 1364   e. wcel 2164   {cab 2179   _Vcvv 2760   {csn 3618   {cpr 3619   <.cop 3621

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627

This theorem is referenced by:  opeq12  3806  opeq2i  3808  opeq2d  3811  oteq2  3814  oteq3  3815  breq2  4033  cbvopab2  4103  cbvopab2v  4106  opthg  4267  eqvinop  4272  opelopabsb  4290  opelxp  4689  opabid2  4793  elrn2g  4852  opeldm  4865  opeldmg  4867  elrn2  4904  opelresg  4949  iss  4988  elimasng  5033  issref  5048  dmsnopg  5137  cnvsng  5151  elxp4  5153  elxp5  5154  dffun5r  5266  funopg  5288  f1osng  5541  tz6.12f  5583  fsn  5730  fsng  5731  fvsng  5754  oveq2  5926  cbvoprab2  5991  ovg  6057  opabex3d  6173  opabex3  6174  op1stg  6203  op2ndg  6204  oprssdmm  6224  op1steq  6232  dfoprab4f  6246  tfrlemibxssdm  6380  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  elixpsn  6789  ixpsnf1o  6790  mapsnen  6865  xpsnen  6875  xpassen  6884  xpf1o  6900  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djulclb  7114  inl11  7124  djuss  7129  1stinl  7133  2ndinl  7134  1stinr  7135  2ndinr  7136  elreal  7888  ax1rid  7937  fseq1p1m1  10160  imasaddfnlemg  12897  cnmpt21  14459  djucllem  15292