Theorem opeq2i 4808

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

Hypothesis

Ref	Expression
opeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
opeq2i	⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩

Proof of Theorem opeq2i

Step	Hyp	Ref	Expression
1		opeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		opeq2 4805	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	ax-mp 5	1 ⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩

Syntax hints:   = wceq 1547  ⟨cop 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562

This theorem is referenced by:  fnressn  7101  fressnfv  7103  seqomlem1  8379  recmulnq  10878  addresr  11052  seqval  13965  ids1  14551  pfx1  14656  pfxccatpfx2  14690  ressinbas  17206  oduval  18245  mgmnsgrpex  18893  sgrpnmndex  18894  efgi0  19686  efgi1  19687  vrgpinv  19735  frgpnabllem1  19839  pzriprng1ALT  21471  mat1dimid  22457  seqsval  28298  uspgr1v1eop  29336  wlk2v2e  30245  avril1  30551  nvop  30765  phop  30907  selvply1rhm0  33710  bnj601  35102  tgrpset  41237  erngset  41292  erngset-rN  41300  nregmodelf1o  45459  stgr0  48451  stgr1  48452  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  gpg5edgnedg  48621  zlmodzxzadd  48849  lmod1  48983  lmod1zr  48984  zlmodzxzequa  48987  zlmodzxzequap  48990  cofuoppf  49640  termcfuncval  50022  termcnatval  50025  termolmd  50160