Theorem opeq2i 4800

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

Syntax hints:   = wceq 1533  ⟨cop 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567

This theorem is referenced by:  fnressn  6914  fressnfv  6916  wfrlem14  7962  seqomlem1  8080  recmulnq  10380  addresr  10554  seqval  13374  ids1  13945  pfx1  14059  pfxccatpfx2  14093  ressinbas  16554  oduval  17734  mgmnsgrpex  18090  sgrpnmndex  18091  efgi0  18840  efgi1  18841  vrgpinv  18889  frgpnabllem1  18987  mat1dimid  21077  uspgr1v1eop  27025  wlk2v2e  27930  avril1  28236  nvop  28447  phop  28589  bnj601  32187  tgrpset  37875  erngset  37930  erngset-rN  37938  zlmodzxzadd  44400  lmod1  44541  lmod1zr  44542  zlmodzxzequa  44545  zlmodzxzequap  44548