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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  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  7155  fressnfv  7157  seqomlem1  8439  recmulnq  10973  addresr  11147  seqval  14076  ids1  14664  pfx1  14772  pfxccatpfx2  14806  ressinbas  17337  oduval  18376  mgmnsgrpex  19043  sgrpnmndex  19044  efgi0  19847  efgi1  19848  vrgpinv  19896  frgpnabllem1  20000  pzriprng1ALT  21709  mat1dimid  22696  seqsval  28553  uspgr1v1eop  29709  wlk2v2e  30637  avril1  30943  nvop  31157  phop  31299  selvply1rhm0  34036  bnj601  35429  tgrpset  41618  erngset  41673  erngset-rN  41681  nregmodelf1o  45838  stgr0  48876  stgr1  48877  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  gpg5edgnedg  49046  zlmodzxzadd  49288  lmod1  49422  lmod1zr  49423  zlmodzxzequa  49426  zlmodzxzequap  49429  cofuoppf  50076  termcfuncval  50458  termcnatval  50461  termolmd  50596