Theorem opeq1d 4880

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  oteq1  4883  oteq2  4884  opth  5477  elsnxp  6291  cbvoprab2  7497  fvproj  8120  unxpdomlem1  9250  djulf1o  9907  djurf1o  9908  mulcanenq  10955  ax1rid  11156  axrnegex  11157  fseq1m1p1  13576  uzrdglem  13922  pfxswrd  14656  swrdccat  14685  swrdccat3blem  14689  cshw0  14744  cshwmodn  14745  s2prop  14858  s4prop  14861  fsum2dlem  15716  fprod2dlem  15924  ruclem1  16174  imasaddvallem  17475  iscatd2  17625  moni  17683  homadmcd  17992  curf1  18178  curf1cl  18181  curf2  18182  hofcl  18212  gsum2dlem2  19839  imasdsf1olem  23879  ovoliunlem1  25019  cxpcn3  26256  nosupbnd2  27219  noinfbnd2  27234  axlowdimlem15  28214  axlowdim  28219  nvi  29867  nvop  29929  phop  30071  br8d  31839  fgreu  31897  1stpreimas  31927  smatfval  32775  smatrcl  32776  smatlem  32777  fmla0xp  34374  mvhfval  34524  mpst123  34531  br8  34726  fvtransport  35004  bj-inftyexpitaudisj  36086  rfovcnvf1od  42755  pzriprnglem10  46814