Theorem opeq2i 4406

Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1i.1	|- A = B

Assertion

Ref	Expression
opeq2i	|- <. C , A >. = <. C , B >.

Proof of Theorem opeq2i

Step	Hyp	Ref	Expression
1		opeq1i.1	. 2 |- A = B
2		opeq2 4403	. 2 |- ( A = B -> <. C , A >. = <. C , B >. )
3	1, 2	ax-mp 5	1 |- <. C , A >. = <. C , B >.

Syntax hints:   = wceq 1483   <.cop 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184

This theorem is referenced by:  fnressn  6425  fressnfv  6427  wfrlem14  7428  seqomlem1  7545  recmulnq  9786  addresr  9959  seqval  12812  ids1  13377  wrdeqs1cat  13474  swrdccat3a  13494  ressinbas  15936  oduval  17130  mgmnsgrpex  17418  sgrpnmndex  17419  efgi0  18133  efgi1  18134  vrgpinv  18182  frgpnabllem1  18276  mat1dimid  20280  uspgr1v1eop  26141  clwlksfoclwwlk  26963  wlk2v2e  27017  avril1  27319  nvop  27531  phop  27673  signstfveq0  30654  bnj601  30990  tgrpset  36033  erngset  36088  erngset-rN  36096  pfx1  41411  pfxccatpfx2  41428  zlmodzxzadd  42136  lmod1  42281  lmod1zr  42282  zlmodzxzequa  42285  zlmodzxzequap  42288