Theorem opeq2i 4853

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

Syntax hints:   = wceq 1540  ⟨cop 4607

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  fnressn  7148  fressnfv  7150  wfrlem14OLD  8336  seqomlem1  8464  recmulnq  10978  addresr  11152  seqval  14030  ids1  14615  pfx1  14721  pfxccatpfx2  14755  ressinbas  17266  oduval  18300  mgmnsgrpex  18909  sgrpnmndex  18910  efgi0  19701  efgi1  19702  vrgpinv  19750  frgpnabllem1  19854  dfcnfldOLD  21331  pzriprng1ALT  21457  mat1dimid  22412  seqsval  28234  uspgr1v1eop  29228  wlk2v2e  30138  avril1  30444  nvop  30657  phop  30799  bnj601  34951  tgrpset  40764  erngset  40819  erngset-rN  40827  stgr0  47972  stgr1  47973  zlmodzxzadd  48333  lmod1  48468  lmod1zr  48469  zlmodzxzequa  48472  zlmodzxzequap  48475  termcfuncval  49417  termcnatval  49420