Theorem opeq2i 4338

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

Syntax hints:   = wceq 1474  ⟨cop 4130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131

This theorem is referenced by:  fnressn  6308  fressnfv  6310  wfrlem14  7292  seqomlem1  7409  recmulnq  9642  addresr  9815  seqval  12629  ids1  13176  wrdeqs1cat  13272  swrdccat3a  13291  ressinbas  15709  oduval  16899  mgmnsgrpex  17187  sgrpnmndex  17188  efgi0  17902  efgi1  17903  vrgpinv  17951  frgpnabllem1  18045  mat1dimid  20041  clwlkfoclwwlk  26138  vdgr1c  26198  avril1  26477  nvop  26710  phop  26863  signstfveq0  29786  bnj601  30050  tgrpset  34847  erngset  34902  erngset-rN  34910  pfx1  40072  pfxccatpfx2  40089  uspgr1v1eop  40470  clwlksfoclwwlk  41265  1wlk2v2e  41319  zlmodzxzadd  41924  lmod1  42070  lmod1zr  42071  zlmodzxzequa  42074  zlmodzxzequap  42077