Theorem opeq2i 4901

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

Syntax hints:   = wceq 1537  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  fnressn  7192  fressnfv  7194  wfrlem14OLD  8378  seqomlem1  8506  recmulnq  11033  addresr  11207  seqval  14063  ids1  14645  pfx1  14751  pfxccatpfx2  14785  ressinbas  17304  oduval  18358  mgmnsgrpex  18966  sgrpnmndex  18967  efgi0  19762  efgi1  19763  vrgpinv  19811  frgpnabllem1  19915  dfcnfldOLD  21403  pzriprng1ALT  21530  mat1dimid  22501  seqsval  28312  uspgr1v1eop  29284  wlk2v2e  30189  avril1  30495  nvop  30708  phop  30850  bnj601  34896  tgrpset  40702  erngset  40757  erngset-rN  40765  zlmodzxzadd  48083  lmod1  48221  lmod1zr  48222  zlmodzxzequa  48225  zlmodzxzequap  48228