Theorem opeq2i 4837

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

This proof depends on syntax axioms:   = wceq 1570  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  fnressn  7162  fressnfv  7164  seqomlem1  8460  recmulnq  11049  addresr  11223  seqval  14155  ids1  14744  pfx1  14852  pfxccatpfx2  14886  ressinbas  17423  oduval  18462  mgmnsgrpex  19130  sgrpnmndex  19131  efgi0  19934  efgi1  19935  vrgpinv  19983  frgpnabllem1  20087  pzriprng1ALT  21802  mat1dimid  22789  seqsval  28674  uspgr1v1eop  29830  wlk2v2e  30758  avril1  31064  nvop  31278  phop  31420  selvply1rhm0  34158  bnj601  35550  tgrpset  41802  erngset  41857  erngset-rN  41865  nregmodelf1o  46004  stgr0  49057  stgr1  49058  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  gpg5edgnedg  49227  zlmodzxzadd  49469  lmod1  49603  lmod1zr  49604  zlmodzxzequa  49607  zlmodzxzequap  49610  cofuoppf  50257  termcfuncval  50639  termcnatval  50642  termolmd  50777