Theorem opeq2i 4841

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

Syntax hints:   = wceq 1540  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  fnressn  7130  fressnfv  7132  seqomlem1  8418  recmulnq  10917  addresr  11091  seqval  13977  ids1  14562  pfx1  14668  pfxccatpfx2  14702  ressinbas  17215  oduval  18249  mgmnsgrpex  18858  sgrpnmndex  18859  efgi0  19650  efgi1  19651  vrgpinv  19699  frgpnabllem1  19803  dfcnfldOLD  21280  pzriprng1ALT  21406  mat1dimid  22361  seqsval  28182  uspgr1v1eop  29176  wlk2v2e  30086  avril1  30392  nvop  30605  phop  30747  bnj601  34910  tgrpset  40739  erngset  40794  erngset-rN  40802  nregmodelf1o  45005  stgr0  47959  stgr1  47960  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  zlmodzxzadd  48346  lmod1  48481  lmod1zr  48482  zlmodzxzequa  48485  zlmodzxzequap  48488  cofuoppf  49139  termcfuncval  49521  termcnatval  49524  termolmd  49659