Theorem opeq2d 3906

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

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq2d	⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq2 3900	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1402  ⟨cop 3708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714

This theorem is referenced by:  tfr1onlemaccex  6609  tfrcllemaccex  6622  fundmen  7084  exmidapne  7616  recexnq  7747  suplocexprlemex  8079  elreal2  8187  frecuzrdgrrn  10823  frec2uzrdg  10824  frecuzrdgrcl  10825  frecuzrdgsuc  10829  frecuzrdgrclt  10830  frecuzrdgg  10831  frecuzrdgsuctlem  10838  seqeq2  10866  seqeq3  10867  iseqvalcbv  10874  seq3val  10875  seqvalcd  10876  s1val  11363  s1eq  11365  s1prc  11369  swrdlsw  11419  pfxpfx  11458  swrdccat  11485  swrdccat3blem  11489  swrdccat3b  11490  pfxccatin12d  11495  eucalgval  12810  ennnfonelemp1  13275  ennnfonelemnn0  13291  strsetsid  13363  ressvalsets  13395  strressid  13402  ressinbasd  13405  ressressg  13406  imasex  13603  imasival  13604  imasaddvallemg  13613  xpsfval  13646  prdsex  14149  prdsval  14150  xpsval  14178  mgpvalg  14197  mgpress  14205  ring1  14337  opprvalg  14347  sraval  14746  zlmval  14934  znval  14943  znval2  14945  psrval  14973  upgr1een  16279  uspgr1ewopdc  16399  usgr2v1e2w  16401  1loopgruspgr  16458  eupth2lem3lem3fi  16625  eupth2fi  16634