Theorem opeq2i 4344

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

Syntax hints:   = wceq 1475  ⟨cop 4131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132

This theorem is referenced by:  fnressn  6330  fressnfv  6332  wfrlem14  7315  seqomlem1  7432  recmulnq  9665  addresr  9838  seqval  12674  ids1  13230  wrdeqs1cat  13326  swrdccat3a  13345  ressinbas  15763  oduval  16953  mgmnsgrpex  17241  sgrpnmndex  17242  efgi0  17956  efgi1  17957  vrgpinv  18005  frgpnabllem1  18099  mat1dimid  20099  clwlkfoclwwlk  26372  vdgr1c  26432  avril1  26711  nvop  26915  phop  27057  signstfveq0  29980  bnj601  30244  tgrpset  35051  erngset  35106  erngset-rN  35114  pfx1  40274  pfxccatpfx2  40291  uspgr1v1eop  40475  clwlksfoclwwlk  41270  1wlk2v2e  41324  zlmodzxzadd  41929  lmod1  42075  lmod1zr  42076  zlmodzxzequa  42079  zlmodzxzequap  42082