Theorem opeq2i 4835

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

Syntax hints:   = wceq 1560  ⟨cop 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  fnressn  7141  fressnfv  7143  seqomlem1  8421  recmulnq  10922  addresr  11096  seqval  14025  ids1  14611  pfx1  14716  pfxccatpfx2  14750  ressinbas  17281  oduval  18320  mgmnsgrpex  18968  sgrpnmndex  18969  efgi0  19760  efgi1  19761  vrgpinv  19809  frgpnabllem1  19913  pzriprng1ALT  21545  mat1dimid  22531  seqsval  28378  uspgr1v1eop  29447  wlk2v2e  30356  avril1  30662  nvop  30876  phop  31018  selvply1rhm0  33820  bnj601  35212  tgrpset  41366  erngset  41421  erngset-rN  41429  nregmodelf1o  45588  stgr0  48579  stgr1  48580  pgnbgreunbgrlem2lem1  48733  pgnbgreunbgrlem2lem2  48734  gpg5edgnedg  48749  zlmodzxzadd  48977  lmod1  49111  lmod1zr  49112  zlmodzxzequa  49115  zlmodzxzequap  49118  cofuoppf  49768  termcfuncval  50150  termcnatval  50153  termolmd  50288