Theorem opeq2i 4882

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

Syntax hints:   = wceq 1537  ⟨cop 4637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638

This theorem is referenced by:  fnressn  7178  fressnfv  7180  wfrlem14OLD  8361  seqomlem1  8489  recmulnq  11002  addresr  11176  seqval  14050  ids1  14632  pfx1  14738  pfxccatpfx2  14772  ressinbas  17291  oduval  18345  mgmnsgrpex  18957  sgrpnmndex  18958  efgi0  19753  efgi1  19754  vrgpinv  19802  frgpnabllem1  19906  dfcnfldOLD  21398  pzriprng1ALT  21525  mat1dimid  22496  seqsval  28309  uspgr1v1eop  29281  wlk2v2e  30186  avril1  30492  nvop  30705  phop  30847  bnj601  34913  tgrpset  40728  erngset  40783  erngset-rN  40791  stgr0  47863  stgr1  47864  zlmodzxzadd  48203  lmod1  48338  lmod1zr  48339  zlmodzxzequa  48342  zlmodzxzequap  48345