Theorem opeq2i 4846

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

Syntax hints:   = wceq 1567  ⟨cop 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is referenced by:  fnressn  7158  fressnfv  7160  seqomlem1  8439  recmulnq  10951  addresr  11125  seqval  14050  ids1  14637  pfx1  14742  pfxccatpfx2  14776  ressinbas  17307  oduval  18346  mgmnsgrpex  18995  sgrpnmndex  18996  efgi0  19792  efgi1  19793  vrgpinv  19841  frgpnabllem1  19945  pzriprng1ALT  21617  mat1dimid  22602  seqsval  28449  uspgr1v1eop  29542  wlk2v2e  30451  avril1  30757  nvop  30971  phop  31113  selvply1rhm0  33863  bnj601  35255  tgrpset  41446  erngset  41501  erngset-rN  41509  nregmodelf1o  45653  stgr0  48651  stgr1  48652  pgnbgreunbgrlem2lem1  48805  pgnbgreunbgrlem2lem2  48806  gpg5edgnedg  48821  zlmodzxzadd  49060  lmod1  49194  lmod1zr  49195  zlmodzxzequa  49198  zlmodzxzequap  49201  cofuoppf  49850  termcfuncval  50232  termcnatval  50235  termolmd  50370