Theorem opeq2i 4557

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

Syntax hints:   = wceq 1632  ⟨cop 4327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328

This theorem is referenced by:  fnressn  6588  fressnfv  6590  wfrlem14  7597  seqomlem1  7714  recmulnq  9978  addresr  10151  seqval  13006  ids1  13567  wrdeqs1cat  13674  swrdccat3a  13694  ressinbas  16138  oduval  17331  mgmnsgrpex  17619  sgrpnmndex  17620  efgi0  18333  efgi1  18334  vrgpinv  18382  frgpnabllem1  18476  mat1dimid  20482  uspgr1v1eop  26340  clwlkclwwlkfo  27132  clwlksfoclwwlkOLD  27217  wlk2v2e  27309  avril1  27630  nvop  27840  phop  27982  signstfveq0  30963  bnj601  31297  tgrpset  36535  erngset  36590  erngset-rN  36598  pfx1  41921  pfxccatpfx2  41938  zlmodzxzadd  42646  lmod1  42791  lmod1zr  42792  zlmodzxzequa  42795  zlmodzxzequap  42798