Theorem opeq1d 4879

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

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

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635

This theorem is referenced by:  oteq1  4882  oteq2  4883  opth  5476  elsnxp  6288  cbvoprab2  7494  fvproj  8117  unxpdomlem1  9247  djulf1o  9904  djurf1o  9905  mulcanenq  10952  ax1rid  11153  axrnegex  11154  fseq1m1p1  13573  uzrdglem  13919  pfxswrd  14653  swrdccat  14682  swrdccat3blem  14686  cshw0  14741  cshwmodn  14742  s2prop  14855  s4prop  14858  fsum2dlem  15713  fprod2dlem  15921  ruclem1  16171  imasaddvallem  17472  iscatd2  17622  moni  17680  homadmcd  17989  curf1  18175  curf1cl  18178  curf2  18179  hofcl  18209  gsum2dlem2  19834  imasdsf1olem  23871  ovoliunlem1  25011  cxpcn3  26246  nosupbnd2  27209  noinfbnd2  27224  axlowdimlem15  28204  axlowdim  28209  nvi  29855  nvop  29917  phop  30059  br8d  31827  fgreu  31885  1stpreimas  31915  smatfval  32764  smatrcl  32765  smatlem  32766  fmla0xp  34363  mvhfval  34513  mpst123  34520  br8  34715  fvtransport  34993  bj-inftyexpitaudisj  36075  rfovcnvf1od  42741