Theorem opeq1d 4833

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  oteq1  4836  oteq2  4837  opth  5423  elsnxp  6243  cbvoprab2  7441  cbvoprab12v  7443  fvproj  8074  unxpdomlem1  9155  djulf1o  9827  djurf1o  9828  mulcanenq  10873  ax1rid  11074  axrnegex  11075  fseq1m1p1  13520  uzrdglem  13882  pfxswrd  14630  swrdccat  14659  swrdccat3blem  14663  cshw0  14718  cshwmodn  14719  s2prop  14832  s4prop  14835  fsum2dlem  15695  fprod2dlem  15905  ruclem1  16158  imasaddvallem  17451  iscatd2  17605  moni  17661  homadmcd  17967  curf1  18149  curf1cl  18152  curf2  18153  hofcl  18183  gsum2dlem2  19868  pzriprnglem10  21415  imasdsf1olem  24277  ovoliunlem1  25419  cxpcn3  26674  nosupbnd2  27644  noinfbnd2  27659  noseqrdglem  28222  axlowdimlem15  28919  axlowdim  28924  nvi  30576  nvop  30638  phop  30780  br8d  32571  fgreu  32629  1stpreimas  32662  rlocval  33212  rloccring  33223  smatfval  33764  smatrcl  33765  smatlem  33766  fmla0xp  35358  mvhfval  35508  mpst123  35515  br8  35731  fvtransport  36008  cbvoprab1vw  36213  cbvoprab2vw  36214  cbvoprab1davw  36247  cbvoprab2davw  36248  cbvoprab12davw  36251  bj-inftyexpitaudisj  37181  rfovcnvf1od  43980  oppcup3lem  49195  tposcurf2val  49290  oppcthinendcALT  49430  concom  49652