Theorem opeq2i 4844

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  fnressn  7161  fressnfv  7163  seqomlem1  8443  recmulnq  10964  addresr  11138  seqval  14066  ids1  14654  pfx1  14762  pfxccatpfx2  14796  ressinbas  17327  oduval  18366  mgmnsgrpex  19030  sgrpnmndex  19031  efgi0  19834  efgi1  19835  vrgpinv  19883  frgpnabllem1  19987  pzriprng1ALT  21696  mat1dimid  22681  seqsval  28532  uspgr1v1eop  29657  wlk2v2e  30579  avril1  30885  nvop  31099  phop  31241  selvply1rhm0  33980  bnj601  35373  tgrpset  41577  erngset  41632  erngset-rN  41640  nregmodelf1o  45782  stgr0  48783  stgr1  48784  pgnbgreunbgrlem2lem1  48937  pgnbgreunbgrlem2lem2  48938  gpg5edgnedg  48953  zlmodzxzadd  49195  lmod1  49329  lmod1zr  49330  zlmodzxzequa  49333  zlmodzxzequap  49336  cofuoppf  49985  termcfuncval  50367  termcnatval  50370  termolmd  50505