Theorem opeq2d 3812

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

Syntax hints:   → wi 4   = wceq 1364  ⟨cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  tfr1onlemaccex  6403  tfrcllemaccex  6416  fundmen  6862  exmidapne  7322  recexnq  7452  suplocexprlemex  7784  elreal2  7892  frecuzrdgrrn  10482  frec2uzrdg  10483  frecuzrdgrcl  10484  frecuzrdgsuc  10488  frecuzrdgrclt  10489  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seqeq2  10525  seqeq3  10526  iseqvalcbv  10533  seq3val  10534  seqvalcd  10535  eucalgval  12195  ennnfonelemp1  12566  ennnfonelemnn0  12582  strsetsid  12654  ressvalsets  12685  strressid  12692  ressinbasd  12695  ressressg  12696  prdsex  12883  imasex  12891  imasival  12892  imasaddvallemg  12901  xpsfval  12934  xpsval  12938  mgpvalg  13422  mgpress  13430  ring1  13558  opprvalg  13568  sraval  13936  zlmval  14126  znval  14135  znval2  14137  psrval  14163