Theorem opeq2i 4842

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

Syntax hints:   = wceq 1570  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  fnressn  7155  fressnfv  7157  seqomlem1  8433  recmulnq  10944  addresr  11118  seqval  14044  ids1  14631  pfx1  14736  pfxccatpfx2  14770  ressinbas  17300  oduval  18339  mgmnsgrpex  18988  sgrpnmndex  18989  efgi0  19785  efgi1  19786  vrgpinv  19834  frgpnabllem1  19938  pzriprng1ALT  21646  mat1dimid  22631  seqsval  28481  uspgr1v1eop  29599  wlk2v2e  30508  avril1  30814  nvop  31028  phop  31170  selvply1rhm0  33916  bnj601  35308  tgrpset  41519  erngset  41574  erngset-rN  41582  nregmodelf1o  45724  stgr0  48725  stgr1  48726  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  gpg5edgnedg  48895  zlmodzxzadd  49138  lmod1  49272  lmod1zr  49273  zlmodzxzequa  49276  zlmodzxzequap  49279  cofuoppf  49928  termcfuncval  50310  termcnatval  50313  termolmd  50448