Theorem opeq1d 4845

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

Syntax hints:   → wi 4   = wceq 1570  ⟨cop 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597

This theorem is referenced by:  oteq1  4848  oteq2  4849  opth  5460  elsnxp  6294  cbvoprab2  7500  cbvoprab12v  7502  fvproj  8131  unxpdomlem1  9217  djulf1o  9899  djurf1o  9900  mulcanenq  10946  ax1rid  11147  axrnegex  11148  fseq1m1p1  13629  uzrdglem  13995  pfxswrd  14745  swrdccat  14774  swrdccat3blem  14778  cshw0  14833  cshwmodn  14834  s2prop  14946  s4prop  14949  fsum2dlem  15823  fprod2dlem  16036  ruclem1  16288  imasaddvallem  17584  iscatd2  17738  moni  17794  homadmcd  18100  curf1  18282  curf1cl  18285  curf2  18286  hofcl  18316  gsum2dlem2  20042  pzriprnglem10  21621  imasdsf1olem  24511  ovoliunlem1  25642  cxpcn3  26894  nosupbnd2  27861  noinfbnd2  27876  noseqrdglem  28479  axlowdimlem15  29287  axlowdim  29292  nvi  30947  nvop  31009  phop  31151  br8d  32934  fgreu  32997  1stpreimas  33032  rlocval  33560  rloccring  33572  smatfval  34166  smatrcl  34167  smatlem  34168  fmla0xp  35856  mvhfval  36006  mpst123  36013  br8  36229  fvtransport  36505  cbvoprab1vw  36730  cbvoprab2vw  36731  cbvoprab1davw  36764  cbvoprab2davw  36765  cbvoprab12davw  36768  bj-inftyexpitaudisj  37830  rfovcnvf1od  44713  oppcup3lem  49967  tposcurf2val  50062  oppcthinendcALT  50202  concom  50424