Theorem opeq2i 4828

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

Syntax hints:   = wceq 1540  ⟨cop 4583

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  fnressn  7092  fressnfv  7094  seqomlem1  8372  recmulnq  10858  addresr  11032  seqval  13919  ids1  14504  pfx1  14609  pfxccatpfx2  14643  ressinbas  17156  oduval  18194  mgmnsgrpex  18805  sgrpnmndex  18806  efgi0  19599  efgi1  19600  vrgpinv  19648  frgpnabllem1  19752  dfcnfldOLD  21277  pzriprng1ALT  21403  mat1dimid  22359  seqsval  28187  uspgr1v1eop  29194  wlk2v2e  30101  avril1  30407  nvop  30620  phop  30762  bnj601  34887  tgrpset  40724  erngset  40779  erngset-rN  40787  nregmodelf1o  44989  stgr0  47944  stgr1  47945  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  gpg5edgnedg  48114  zlmodzxzadd  48342  lmod1  48477  lmod1zr  48478  zlmodzxzequa  48481  zlmodzxzequap  48484  cofuoppf  49135  termcfuncval  49517  termcnatval  49520  termolmd  49655