Theorem opeq2i 4831

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 4828	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	ax-mp 5	1 ⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩

Syntax hints:   = wceq 1541  ⟨cop 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585

This theorem is referenced by:  fnressn  7101  fressnfv  7103  seqomlem1  8379  recmulnq  10873  addresr  11047  seqval  13933  ids1  14519  pfx1  14624  pfxccatpfx2  14658  ressinbas  17170  oduval  18209  mgmnsgrpex  18854  sgrpnmndex  18855  efgi0  19647  efgi1  19648  vrgpinv  19696  frgpnabllem1  19800  dfcnfldOLD  21323  pzriprng1ALT  21449  mat1dimid  22416  seqsval  28249  uspgr1v1eop  29271  wlk2v2e  30181  avril1  30487  nvop  30700  phop  30842  bnj601  35025  tgrpset  40944  erngset  40999  erngset-rN  41007  nregmodelf1o  45198  stgr0  48148  stgr1  48149  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  gpg5edgnedg  48318  zlmodzxzadd  48546  lmod1  48680  lmod1zr  48681  zlmodzxzequa  48684  zlmodzxzequap  48687  cofuoppf  49337  termcfuncval  49719  termcnatval  49722  termolmd  49857