Theorem opeq2d 3863

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

Syntax hints:   → wi 4   = wceq 1395  ⟨cop 3669

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675

This theorem is referenced by:  tfr1onlemaccex  6492  tfrcllemaccex  6505  fundmen  6957  exmidapne  7442  recexnq  7573  suplocexprlemex  7905  elreal2  8013  frecuzrdgrrn  10625  frec2uzrdg  10626  frecuzrdgrcl  10627  frecuzrdgsuc  10631  frecuzrdgrclt  10632  frecuzrdgg  10633  frecuzrdgsuctlem  10640  seqeq2  10668  seqeq3  10669  iseqvalcbv  10676  seq3val  10677  seqvalcd  10678  s1val  11145  s1eq  11147  s1prc  11151  swrdlsw  11196  pfxpfx  11235  swrdccat  11262  swrdccat3blem  11266  swrdccat3b  11267  pfxccatin12d  11272  eucalgval  12571  ennnfonelemp1  12972  ennnfonelemnn0  12988  strsetsid  13060  ressvalsets  13092  strressid  13099  ressinbasd  13102  ressressg  13103  prdsex  13297  prdsval  13301  imasex  13333  imasival  13334  imasaddvallemg  13343  xpsfval  13376  xpsval  13380  mgpvalg  13881  mgpress  13889  ring1  14017  opprvalg  14027  sraval  14395  zlmval  14585  znval  14594  znval2  14596  psrval  14624