Theorem opeq1d 4855

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  oteq1  4858  oteq2  4859  opth  5451  elsnxp  6280  cbvoprab2  7495  cbvoprab12v  7497  fvproj  8133  unxpdomlem1  9258  djulf1o  9926  djurf1o  9927  mulcanenq  10974  ax1rid  11175  axrnegex  11176  fseq1m1p1  13616  uzrdglem  13975  pfxswrd  14724  swrdccat  14753  swrdccat3blem  14757  cshw0  14812  cshwmodn  14813  s2prop  14926  s4prop  14929  fsum2dlem  15786  fprod2dlem  15996  ruclem1  16249  imasaddvallem  17543  iscatd2  17693  moni  17749  homadmcd  18055  curf1  18237  curf1cl  18240  curf2  18241  hofcl  18271  gsum2dlem2  19952  pzriprnglem10  21451  imasdsf1olem  24312  ovoliunlem1  25455  cxpcn3  26710  nosupbnd2  27680  noinfbnd2  27695  noseqrdglem  28251  axlowdimlem15  28935  axlowdim  28940  nvi  30595  nvop  30657  phop  30799  br8d  32590  fgreu  32650  1stpreimas  32683  rlocval  33254  rloccring  33265  smatfval  33826  smatrcl  33827  smatlem  33828  fmla0xp  35405  mvhfval  35555  mpst123  35562  br8  35773  fvtransport  36050  cbvoprab1vw  36255  cbvoprab2vw  36256  cbvoprab1davw  36289  cbvoprab2davw  36290  cbvoprab12davw  36293  bj-inftyexpitaudisj  37223  rfovcnvf1od  44028  oppcup3lem  49139  tposcurf2val  49212  oppcthinendcALT  49327  concom  49533