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  7156  fressnfv  7158  seqomlem1  8436  recmulnq  10948  addresr  11122  seqval  14047  ids1  14634  pfx1  14739  pfxccatpfx2  14773  ressinbas  17304  oduval  18343  mgmnsgrpex  18992  sgrpnmndex  18993  efgi0  19789  efgi1  19790  vrgpinv  19838  frgpnabllem1  19942  pzriprng1ALT  21614  mat1dimid  22599  seqsval  28446  uspgr1v1eop  29539  wlk2v2e  30448  avril1  30754  nvop  30968  phop  31110  selvply1rhm0  33860  bnj601  35252  tgrpset  41408  erngset  41463  erngset-rN  41471  nregmodelf1o  45615  stgr0  48613  stgr1  48614  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  gpg5edgnedg  48783  zlmodzxzadd  49022  lmod1  49156  lmod1zr  49157  zlmodzxzequa  49160  zlmodzxzequap  49163  cofuoppf  49812  termcfuncval  50194  termcnatval  50197  termolmd  50332