Theorem opeq2i 4437

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

Syntax hints:   = wceq 1523  ⟨cop 4216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217

This theorem is referenced by:  fnressn  6465  fressnfv  6467  wfrlem14  7473  seqomlem1  7590  recmulnq  9824  addresr  9997  seqval  12852  ids1  13413  wrdeqs1cat  13520  swrdccat3a  13540  ressinbas  15983  oduval  17177  mgmnsgrpex  17465  sgrpnmndex  17466  efgi0  18179  efgi1  18180  vrgpinv  18228  frgpnabllem1  18322  mat1dimid  20328  uspgr1v1eop  26186  clwlksfoclwwlk  27050  wlk2v2e  27135  avril1  27449  nvop  27659  phop  27801  signstfveq0  30782  bnj601  31116  tgrpset  36350  erngset  36405  erngset-rN  36413  pfx1  41736  pfxccatpfx2  41753  zlmodzxzadd  42461  lmod1  42606  lmod1zr  42607  zlmodzxzequa  42610  zlmodzxzequap  42613