Theorem opeq2i 4876

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

Syntax hints:   = wceq 1541  ⟨cop 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634

This theorem is referenced by:  fnressn  7152  fressnfv  7154  wfrlem14OLD  8318  seqomlem1  8446  recmulnq  10955  addresr  11129  seqval  13973  ids1  14543  pfx1  14649  pfxccatpfx2  14683  ressinbas  17186  oduval  18237  mgmnsgrpex  18808  sgrpnmndex  18809  efgi0  19582  efgi1  19583  vrgpinv  19631  frgpnabllem1  19735  mat1dimid  21967  uspgr1v1eop  28495  wlk2v2e  29399  avril1  29705  nvop  29916  phop  30058  bnj601  33919  tgrpset  39604  erngset  39659  erngset-rN  39667  zlmodzxzadd  46987  lmod1  47126  lmod1zr  47127  zlmodzxzequa  47130  zlmodzxzequap  47133