Theorem opeq1d 4771

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

Syntax hints:   → wi 4   = wceq 1538  ⟨cop 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532

This theorem is referenced by:  oteq1  4774  oteq2  4775  opth  5333  elsnxp  6110  cbvoprab2  7221  fvproj  7811  unxpdomlem1  8706  djulf1o  9325  djurf1o  9326  mulcanenq  10371  ax1rid  10572  axrnegex  10573  fseq1m1p1  12977  uzrdglem  13320  pfxswrd  14059  swrdccat  14088  swrdccat3blem  14092  cshw0  14147  cshwmodn  14148  s2prop  14260  s4prop  14263  fsum2dlem  15117  fprod2dlem  15326  ruclem1  15576  imasaddvallem  16794  iscatd2  16944  moni  16998  homadmcd  17294  curf1  17467  curf1cl  17470  curf2  17471  hofcl  17501  gsum2dlem2  19084  imasdsf1olem  22980  ovoliunlem1  24106  cxpcn3  25337  axlowdimlem15  26750  axlowdim  26755  nvi  28397  nvop  28459  phop  28601  br8d  30374  fgreu  30435  1stpreimas  30465  smatfval  31148  smatrcl  31149  smatlem  31150  fmla0xp  32743  mvhfval  32893  mpst123  32900  br8  33105  nosupbnd2  33329  fvtransport  33606  bj-inftyexpitaudisj  34620  rfovcnvf1od  40705