Theorem opeq2i 4877

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

Syntax hints:   = wceq 1540  ⟨cop 4632

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  fnressn  7178  fressnfv  7180  wfrlem14OLD  8362  seqomlem1  8490  recmulnq  11004  addresr  11178  seqval  14053  ids1  14635  pfx1  14741  pfxccatpfx2  14775  ressinbas  17291  oduval  18333  mgmnsgrpex  18944  sgrpnmndex  18945  efgi0  19738  efgi1  19739  vrgpinv  19787  frgpnabllem1  19891  dfcnfldOLD  21380  pzriprng1ALT  21507  mat1dimid  22480  seqsval  28294  uspgr1v1eop  29266  wlk2v2e  30176  avril1  30482  nvop  30695  phop  30837  bnj601  34934  tgrpset  40747  erngset  40802  erngset-rN  40810  stgr0  47927  stgr1  47928  zlmodzxzadd  48274  lmod1  48409  lmod1zr  48410  zlmodzxzequa  48413  zlmodzxzequap  48416