Theorem opeq1i 4832

Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
opeq1i	⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩

Proof of Theorem opeq1i

Step	Hyp	Ref	Expression
1		opeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		opeq1 4829	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	ax-mp 5	1 ⊢ ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩

Syntax hints:   = wceq 1541  ⟨cop 4586

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  axi2m1  11070  s3tpop  14832  2strop  17156  grpbasex  17212  grpplusgx  17213  mat1dimelbas  22415  mat1dim0  22417  mat1dimid  22418  mat1dimscm  22419  mat1dimmul  22420  indistpsx  22954  nosupcbv  27670  noinfcbv  27685  setsiedg  29109  cusgrsize  29528  mapfzcons  42958