Theorem opeq1d 4810

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

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4567

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568

This theorem is referenced by:  oteq1  4813  oteq2  4814  opth  5391  elsnxp  6194  cbvoprab2  7363  fvproj  7975  unxpdomlem1  9027  djulf1o  9670  djurf1o  9671  mulcanenq  10716  ax1rid  10917  axrnegex  10918  fseq1m1p1  13331  uzrdglem  13677  pfxswrd  14419  swrdccat  14448  swrdccat3blem  14452  cshw0  14507  cshwmodn  14508  s2prop  14620  s4prop  14623  fsum2dlem  15482  fprod2dlem  15690  ruclem1  15940  imasaddvallem  17240  iscatd2  17390  moni  17448  homadmcd  17757  curf1  17943  curf1cl  17946  curf2  17947  hofcl  17977  gsum2dlem2  19572  imasdsf1olem  23526  ovoliunlem1  24666  cxpcn3  25901  axlowdimlem15  27324  axlowdim  27329  nvi  28976  nvop  29038  phop  29180  br8d  30950  fgreu  31009  1stpreimas  31038  smatfval  31745  smatrcl  31746  smatlem  31747  fmla0xp  33345  mvhfval  33495  mpst123  33502  br8  33723  frxp3  33797  xpord3pred  33798  nosupbnd2  33919  noinfbnd2  33934  fvtransport  34334  bj-inftyexpitaudisj  35376  rfovcnvf1od  41612