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  6513  tfrcllemaccex  6526  fundmen  6980  exmidapne  7478  recexnq  7609  suplocexprlemex  7941  elreal2  8049  frecuzrdgrrn  10669  frec2uzrdg  10670  frecuzrdgrcl  10671  frecuzrdgsuc  10675  frecuzrdgrclt  10676  frecuzrdgg  10677  frecuzrdgsuctlem  10684  seqeq2  10712  seqeq3  10713  iseqvalcbv  10720  seq3val  10721  seqvalcd  10722  s1val  11193  s1eq  11195  s1prc  11199  swrdlsw  11249  pfxpfx  11288  swrdccat  11315  swrdccat3blem  11319  swrdccat3b  11320  pfxccatin12d  11325  eucalgval  12625  ennnfonelemp1  13026  ennnfonelemnn0  13042  strsetsid  13114  ressvalsets  13146  strressid  13153  ressinbasd  13156  ressressg  13157  prdsex  13351  prdsval  13355  imasex  13387  imasival  13388  imasaddvallemg  13397  xpsfval  13430  xpsval  13434  mgpvalg  13935  mgpress  13943  ring1  14071  opprvalg  14081  sraval  14450  zlmval  14640  znval  14649  znval2  14651  psrval  14679  upgr1een  15974  uspgr1ewopdc  16094  usgr2v1e2w  16096  1loopgruspgr  16153