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 ⊢ ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩

Syntax hints:   = wceq 1540  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  fnressn  7112  fressnfv  7114  seqomlem1  8395  recmulnq  10893  addresr  11067  seqval  13953  ids1  14538  pfx1  14644  pfxccatpfx2  14678  ressinbas  17191  oduval  18225  mgmnsgrpex  18834  sgrpnmndex  18835  efgi0  19626  efgi1  19627  vrgpinv  19675  frgpnabllem1  19779  dfcnfldOLD  21256  pzriprng1ALT  21382  mat1dimid  22337  seqsval  28158  uspgr1v1eop  29152  wlk2v2e  30059  avril1  30365  nvop  30578  phop  30720  bnj601  34883  tgrpset  40712  erngset  40767  erngset-rN  40775  nregmodelf1o  44978  stgr0  47932  stgr1  47933  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  zlmodzxzadd  48319  lmod1  48454  lmod1zr  48455  zlmodzxzequa  48458  zlmodzxzequap  48461  cofuoppf  49112  termcfuncval  49494  termcnatval  49497  termolmd  49632