Theorem opeq1d 4834

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq1d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq1 4828	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   = wceq 1559  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  oteq1  4837  oteq2  4838  opth  5441  elsnxp  6272  cbvoprab2  7478  cbvoprab12v  7480  fvproj  8107  unxpdomlem1  9193  djulf1o  9863  djurf1o  9864  mulcanenq  10911  ax1rid  11112  axrnegex  11113  fseq1m1p1  13597  uzrdglem  13963  pfxswrd  14712  swrdccat  14741  swrdccat3blem  14745  cshw0  14800  cshwmodn  14801  s2prop  14913  s4prop  14916  fsum2dlem  15787  fprod2dlem  16000  ruclem1  16253  imasaddvallem  17549  iscatd2  17703  moni  17759  homadmcd  18065  curf1  18247  curf1cl  18250  curf2  18251  hofcl  18281  gsum2dlem2  20001  pzriprnglem10  21529  imasdsf1olem  24420  ovoliunlem1  25551  cxpcn3  26800  nosupbnd2  27767  noinfbnd2  27782  noseqrdglem  28385  axlowdimlem15  29113  axlowdim  29118  nvi  30773  nvop  30835  phop  30977  br8d  32770  fgreu  32833  1stpreimas  32868  rlocval  33400  rloccring  33412  smatfval  34052  smatrcl  34053  smatlem  34054  fmla0xp  35693  mvhfval  35843  mpst123  35850  br8  36066  fvtransport  36342  cbvoprab1vw  36557  cbvoprab2vw  36558  cbvoprab1davw  36591  cbvoprab2davw  36592  cbvoprab12davw  36595  bj-inftyexpitaudisj  37657  rfovcnvf1od  44540  oppcup3lem  49787  tposcurf2val  49882  oppcthinendcALT  50022  concom  50244