Theorem opeq2i 4708

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

Syntax hints:   = wceq 1520  ⟨cop 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473

This theorem is referenced by:  fnressn  6774  fressnfv  6776  wfrlem14  7811  seqomlem1  7928  recmulnq  10221  addresr  10395  seqval  13218  ids1  13783  pfx1  13889  pfxccatpfx2  13923  ressinbas  16377  oduval  17557  mgmnsgrpex  17845  sgrpnmndex  17846  efgi0  18561  efgi1  18562  vrgpinv  18610  frgpnabllem1  18704  mat1dimid  20755  uspgr1v1eop  26702  wlk2v2e  27611  avril1  27921  nvop  28132  phop  28274  bnj601  31764  tgrpset  37362  erngset  37417  erngset-rN  37425  zlmodzxzadd  43838  lmod1  43981  lmod1zr  43982  zlmodzxzequa  43985  zlmodzxzequap  43988