Theorem opeq2i 4843

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

This proof depends on syntax axioms:   = wceq 1569  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  fnressn  7167  fressnfv  7169  seqomlem1  8468  recmulnq  11056  addresr  11230  seqval  14162  ids1  14751  pfx1  14860  pfxccatpfx2  14894  ressinbas  17432  oduval  18471  mgmnsgrpex  19139  sgrpnmndex  19140  efgi0  19943  efgi1  19944  vrgpinv  19992  frgpnabllem1  20096  pzriprng1ALT  21811  mat1dimid  22798  seqsval  28683  uspgr1v1eop  29839  wlk2v2e  30767  avril1  31073  nvop  31287  phop  31429  selvply1rhm0  34208  bnj601  35600  tgrpset  41939  erngset  41994  erngset-rN  42002  nregmodelf1o  46141  stgr0  49194  stgr1  49195  pgnbgreunbgrlem2lem1  49348  pgnbgreunbgrlem2lem2  49349  gpg5edgnedg  49364  zlmodzxzadd  49606  lmod1  49740  lmod1zr  49741  zlmodzxzequa  49744  zlmodzxzequap  49747  cofuoppf  50402  termcfuncval  50803  termcnatval  50809  termolmd  50989