Theorem opeq1d 4837

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  oteq1  4840  oteq2  4841  opth  5432  elsnxp  6257  cbvoprab2  7456  cbvoprab12v  7458  fvproj  8086  unxpdomlem1  9168  djulf1o  9836  djurf1o  9837  mulcanenq  10883  ax1rid  11084  axrnegex  11085  fseq1m1p1  13527  uzrdglem  13892  pfxswrd  14641  swrdccat  14670  swrdccat3blem  14674  cshw0  14729  cshwmodn  14730  s2prop  14842  s4prop  14845  fsum2dlem  15705  fprod2dlem  15915  ruclem1  16168  imasaddvallem  17462  iscatd2  17616  moni  17672  homadmcd  17978  curf1  18160  curf1cl  18163  curf2  18164  hofcl  18194  gsum2dlem2  19912  pzriprnglem10  21457  imasdsf1olem  24329  ovoliunlem1  25471  cxpcn3  26726  nosupbnd2  27696  noinfbnd2  27711  noseqrdglem  28313  axlowdimlem15  29041  axlowdim  29046  nvi  30701  nvop  30763  phop  30905  br8d  32697  fgreu  32760  1stpreimas  32795  rlocval  33352  rloccring  33363  smatfval  33972  smatrcl  33973  smatlem  33974  fmla0xp  35596  mvhfval  35746  mpst123  35753  br8  35969  fvtransport  36245  cbvoprab1vw  36450  cbvoprab2vw  36451  cbvoprab1davw  36484  cbvoprab2davw  36485  cbvoprab12davw  36488  bj-inftyexpitaudisj  37457  rfovcnvf1od  44357  oppcup3lem  49562  tposcurf2val  49657  oppcthinendcALT  49797  concom  50019