Theorem opeq2d 3869

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 3863	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 14	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1397  ⟨cop 3672

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  tfr1onlemaccex  6514  tfrcllemaccex  6527  fundmen  6981  exmidapne  7479  recexnq  7610  suplocexprlemex  7942  elreal2  8050  frecuzrdgrrn  10671  frec2uzrdg  10672  frecuzrdgrcl  10673  frecuzrdgsuc  10677  frecuzrdgrclt  10678  frecuzrdgg  10679  frecuzrdgsuctlem  10686  seqeq2  10714  seqeq3  10715  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  s1val  11198  s1eq  11200  s1prc  11204  swrdlsw  11254  pfxpfx  11293  swrdccat  11320  swrdccat3blem  11324  swrdccat3b  11325  pfxccatin12d  11330  eucalgval  12644  ennnfonelemp1  13045  ennnfonelemnn0  13061  strsetsid  13133  ressvalsets  13165  strressid  13172  ressinbasd  13175  ressressg  13176  prdsex  13370  prdsval  13374  imasex  13406  imasival  13407  imasaddvallemg  13416  xpsfval  13449  xpsval  13453  mgpvalg  13955  mgpress  13963  ring1  14091  opprvalg  14101  sraval  14470  zlmval  14660  znval  14669  znval2  14671  psrval  14699  upgr1een  15994  uspgr1ewopdc  16114  usgr2v1e2w  16116  1loopgruspgr  16173  eupth2lem3lem3fi  16340  eupth2fi  16349