Theorem opeq2i 4807

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

Syntax hints:   = wceq 1537  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  fnressn  6920  fressnfv  6922  wfrlem14  7968  seqomlem1  8086  recmulnq  10386  addresr  10560  seqval  13381  ids1  13951  pfx1  14065  pfxccatpfx2  14099  ressinbas  16560  oduval  17740  mgmnsgrpex  18096  sgrpnmndex  18097  efgi0  18846  efgi1  18847  vrgpinv  18895  frgpnabllem1  18993  mat1dimid  21083  uspgr1v1eop  27031  wlk2v2e  27936  avril1  28242  nvop  28453  phop  28595  bnj601  32192  tgrpset  37896  erngset  37951  erngset-rN  37959  zlmodzxzadd  44426  lmod1  44567  lmod1zr  44568  zlmodzxzequa  44571  zlmodzxzequap  44574