Theorem opeq2i 4820

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

Syntax hints:   = wceq 1542  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  fnressn  7112  fressnfv  7114  seqomlem1  8389  recmulnq  10887  addresr  11061  seqval  13974  ids1  14560  pfx1  14665  pfxccatpfx2  14699  ressinbas  17215  oduval  18254  mgmnsgrpex  18902  sgrpnmndex  18903  efgi0  19695  efgi1  19696  vrgpinv  19744  frgpnabllem1  19848  pzriprng1ALT  21476  mat1dimid  22439  seqsval  28280  uspgr1v1eop  29318  wlk2v2e  30227  avril1  30533  nvop  30747  phop  30889  bnj601  35062  tgrpset  41191  erngset  41246  erngset-rN  41254  nregmodelf1o  45442  stgr0  48436  stgr1  48437  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  gpg5edgnedg  48606  zlmodzxzadd  48834  lmod1  48968  lmod1zr  48969  zlmodzxzequa  48972  zlmodzxzequap  48975  cofuoppf  49625  termcfuncval  50007  termcnatval  50010  termolmd  50145