Theorem opeq2i 4826

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

Syntax hints:   = wceq 1541  ⟨cop 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580

This theorem is referenced by:  fnressn  7091  fressnfv  7093  seqomlem1  8369  recmulnq  10855  addresr  11029  seqval  13919  ids1  14505  pfx1  14610  pfxccatpfx2  14644  ressinbas  17156  oduval  18194  mgmnsgrpex  18839  sgrpnmndex  18840  efgi0  19632  efgi1  19633  vrgpinv  19681  frgpnabllem1  19785  dfcnfldOLD  21307  pzriprng1ALT  21433  mat1dimid  22389  seqsval  28218  uspgr1v1eop  29227  wlk2v2e  30137  avril1  30443  nvop  30656  phop  30798  bnj601  34932  tgrpset  40792  erngset  40847  erngset-rN  40855  nregmodelf1o  45056  stgr0  47999  stgr1  48000  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  gpg5edgnedg  48169  zlmodzxzadd  48397  lmod1  48532  lmod1zr  48533  zlmodzxzequa  48536  zlmodzxzequap  48539  cofuoppf  49190  termcfuncval  49572  termcnatval  49575  termolmd  49710