Theorem opeq1d 4849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4838

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839

This theorem is used by:  oteq1  4863  oteq2  4864  opth  5450  elsnxp  6315  cbvoprab2  7534  cbvoprab12v  7536  fvproj  8181  unxpdomlem1  9278  djulf1o  10023  djurf1o  10024  mulcanenq  11075  ax1rid  11276  axrnegex  11277  fseq1m1p1  13763  uzrdglem  14130  pfxswrd  14886  swrdccat  14915  swrdccat3blem  14919  cshw0  14976  cshwmodn  14977  s2prop  15090  s4prop  15093  fsum2dlem  15968  fprod2dlem  16179  ruclem1  16431  imasaddvallem  17733  iscatd2  17887  moni  17943  homadmcd  18249  curf1  18431  curf1cl  18434  curf2  18435  hofcl  18465  gsum2dlem2  20218  pzriprnglem10  21829  imasdsf1olem  24725  ovoliunlem1  25856  cxpcn3  27109  nosupbnd2  28106  noinfbnd2  28121  noseqrdglem  28724  axlowdimlem15  29567  axlowdim  29572  nvi  31249  nvop  31311  phop  31453  br8d  33277  fgreu  33340  1stpreimas  33373  rlocval  33896  rloccring  33908  smatfval  34510  smatrcl  34511  smatlem  34512  ot1st2nd  35808  fmla0xp  36328  mvhfval  36478  mpst123  36485  br8  36712  fvtransport  36988  cbvoprab1vw  37217  cbvoprab2vw  37218  cbvoprab1davw  37251  cbvoprab2davw  37252  cbvoprab12davw  37255  bj-inftyexpitaudisj  38331  rfovcnvf1od  45207  oppcup3lem  50537  tposcurf2val  50638  oppcthinendcALT  50791  parcoval2  50981  concom  51061