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 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  oteq1  4859  oteq2  4860  opth  5444  elsnxp  6294  cbvoprab2  7508  cbvoprab12v  7510  fvproj  8153  unxpdomlem1  9250  djulf1o  9996  djurf1o  9997  mulcanenq  11048  ax1rid  11249  axrnegex  11250  fseq1m1p1  13736  uzrdglem  14103  pfxswrd  14859  swrdccat  14888  swrdccat3blem  14892  cshw0  14949  cshwmodn  14950  s2prop  15063  s4prop  15066  fsum2dlem  15941  fprod2dlem  16152  ruclem1  16404  imasaddvallem  17706  iscatd2  17860  moni  17916  homadmcd  18222  curf1  18404  curf1cl  18407  curf2  18408  hofcl  18438  gsum2dlem2  20190  pzriprnglem10  21801  imasdsf1olem  24697  ovoliunlem1  25828  cxpcn3  27081  nosupbnd2  28078  noinfbnd2  28093  noseqrdglem  28696  axlowdimlem15  29539  axlowdim  29544  nvi  31221  nvop  31283  phop  31425  br8d  33249  fgreu  33312  1stpreimas  33346  rlocval  33866  rloccring  33878  smatfval  34473  smatrcl  34474  smatlem  34475  fmla0xp  36234  mvhfval  36384  mpst123  36391  br8  36613  fvtransport  36889  cbvoprab1vw  37118  cbvoprab2vw  37119  cbvoprab1davw  37152  cbvoprab2davw  37153  cbvoprab12davw  37156  bj-inftyexpitaudisj  38219  rfovcnvf1od  45097  oppcup3lem  50415  tposcurf2val  50516  oppcthinendcALT  50669  parcoval2  50859  concom  50939