Theorem opeq2i 4844

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

Syntax hints:   = wceq 1540  ⟨cop 4598

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  fnressn  7133  fressnfv  7135  seqomlem1  8421  recmulnq  10924  addresr  11098  seqval  13984  ids1  14569  pfx1  14675  pfxccatpfx2  14709  ressinbas  17222  oduval  18256  mgmnsgrpex  18865  sgrpnmndex  18866  efgi0  19657  efgi1  19658  vrgpinv  19706  frgpnabllem1  19810  dfcnfldOLD  21287  pzriprng1ALT  21413  mat1dimid  22368  seqsval  28189  uspgr1v1eop  29183  wlk2v2e  30093  avril1  30399  nvop  30612  phop  30754  bnj601  34917  tgrpset  40746  erngset  40801  erngset-rN  40809  nregmodelf1o  45012  stgr0  47963  stgr1  47964  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  zlmodzxzadd  48350  lmod1  48485  lmod1zr  48486  zlmodzxzequa  48489  zlmodzxzequap  48492  cofuoppf  49143  termcfuncval  49525  termcnatval  49528  termolmd  49663