Theorem opeq2i 4833

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

Syntax hints:   = wceq 1541  ⟨cop 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  fnressn  7103  fressnfv  7105  seqomlem1  8381  recmulnq  10875  addresr  11049  seqval  13935  ids1  14521  pfx1  14626  pfxccatpfx2  14660  ressinbas  17172  oduval  18211  mgmnsgrpex  18856  sgrpnmndex  18857  efgi0  19649  efgi1  19650  vrgpinv  19698  frgpnabllem1  19802  dfcnfldOLD  21325  pzriprng1ALT  21451  mat1dimid  22418  seqsval  28284  uspgr1v1eop  29322  wlk2v2e  30232  avril1  30538  nvop  30751  phop  30893  bnj601  35076  tgrpset  41005  erngset  41060  erngset-rN  41068  nregmodelf1o  45256  stgr0  48206  stgr1  48207  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  gpg5edgnedg  48376  zlmodzxzadd  48604  lmod1  48738  lmod1zr  48739  zlmodzxzequa  48742  zlmodzxzequap  48745  cofuoppf  49395  termcfuncval  49777  termcnatval  49780  termolmd  49915