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 1539  ⟨cop 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  fnressn  7030  fressnfv  7032  wfrlem14OLD  8153  seqomlem1  8281  recmulnq  10720  addresr  10894  seqval  13732  ids1  14302  pfx1  14416  pfxccatpfx2  14450  ressinbas  16955  oduval  18006  mgmnsgrpex  18570  sgrpnmndex  18571  efgi0  19326  efgi1  19327  vrgpinv  19375  frgpnabllem1  19474  mat1dimid  21623  uspgr1v1eop  27616  wlk2v2e  28521  avril1  28827  nvop  29038  phop  29180  bnj601  32900  tgrpset  38759  erngset  38814  erngset-rN  38822  zlmodzxzadd  45694  lmod1  45833  lmod1zr  45834  zlmodzxzequa  45837  zlmodzxzequap  45840