Theorem opeq2i 4878

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

Syntax hints:   = wceq 1542  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  fnressn  7156  fressnfv  7158  wfrlem14OLD  8322  seqomlem1  8450  recmulnq  10959  addresr  11133  seqval  13977  ids1  14547  pfx1  14653  pfxccatpfx2  14687  ressinbas  17190  oduval  18241  mgmnsgrpex  18812  sgrpnmndex  18813  efgi0  19588  efgi1  19589  vrgpinv  19637  frgpnabllem1  19741  mat1dimid  21976  uspgr1v1eop  28537  wlk2v2e  29441  avril1  29747  nvop  29960  phop  30102  bnj601  33962  gg-dfcnfld  35218  tgrpset  39664  erngset  39719  erngset-rN  39727  pzriprng1ALT  46868  zlmodzxzadd  47082  lmod1  47221  lmod1zr  47222  zlmodzxzequa  47225  zlmodzxzequap  47228