Theorem opeq1i 4877

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

Syntax hints:   = wceq 1542  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  axi2m1  11154  s3tpop  14860  2strstr1OLD  17170  2strop1  17172  grpbasex  17236  grpplusgx  17237  mat1dimelbas  21973  mat1dim0  21975  mat1dimid  21976  mat1dimscm  21977  mat1dimmul  21978  indistpsx  22513  nosupcbv  27205  noinfcbv  27220  setsiedg  28296  cusgrsize  28711  mapfzcons  41454