Theorem opeq2d 3874

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

Syntax hints:   → wi 4   = wceq 1398  ⟨cop 3676

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682

This theorem is referenced by:  tfr1onlemaccex  6557  tfrcllemaccex  6570  fundmen  7024  exmidapne  7522  recexnq  7653  suplocexprlemex  7985  elreal2  8093  frecuzrdgrrn  10716  frec2uzrdg  10717  frecuzrdgrcl  10718  frecuzrdgsuc  10722  frecuzrdgrclt  10723  frecuzrdgg  10724  frecuzrdgsuctlem  10731  seqeq2  10759  seqeq3  10760  iseqvalcbv  10767  seq3val  10768  seqvalcd  10769  s1val  11243  s1eq  11245  s1prc  11249  swrdlsw  11299  pfxpfx  11338  swrdccat  11365  swrdccat3blem  11369  swrdccat3b  11370  pfxccatin12d  11375  eucalgval  12689  ennnfonelemp1  13090  ennnfonelemnn0  13106  strsetsid  13178  ressvalsets  13210  strressid  13217  ressinbasd  13220  ressressg  13221  prdsex  13415  prdsval  13419  imasex  13451  imasival  13452  imasaddvallemg  13461  xpsfval  13494  xpsval  13498  mgpvalg  14000  mgpress  14008  ring1  14136  opprvalg  14146  sraval  14516  zlmval  14706  znval  14715  znval2  14717  psrval  14745  upgr1een  16048  uspgr1ewopdc  16168  usgr2v1e2w  16170  1loopgruspgr  16227  eupth2lem3lem3fi  16394  eupth2fi  16403