Theorem opeq1d 4839

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  oteq1  4842  oteq2  4843  opth  5445  elsnxp  6287  cbvoprab2  7500  cbvoprab12v  7502  fvproj  8135  unxpdomlem1  9231  djulf1o  9974  djurf1o  9975  mulcanenq  11026  ax1rid  11227  axrnegex  11228  fseq1m1p1  13713  uzrdglem  14080  pfxswrd  14835  swrdccat  14864  swrdccat3blem  14868  cshw0  14925  cshwmodn  14926  s2prop  15038  s4prop  15041  fsum2dlem  15916  fprod2dlem  16127  ruclem1  16379  imasaddvallem  17681  iscatd2  17835  moni  17891  homadmcd  18197  curf1  18379  curf1cl  18382  curf2  18383  hofcl  18413  gsum2dlem2  20165  pzriprnglem10  21776  imasdsf1olem  24672  ovoliunlem1  25803  cxpcn3  27058  nosupbnd2  28055  noinfbnd2  28070  noseqrdglem  28673  axlowdimlem15  29516  axlowdim  29521  nvi  31198  nvop  31260  phop  31402  br8d  33184  fgreu  33247  1stpreimas  33281  rlocval  33802  rloccring  33814  smatfval  34409  smatrcl  34410  smatlem  34411  fmla0xp  36117  mvhfval  36267  mpst123  36274  br8  36490  fvtransport  36767  cbvoprab1vw  36996  cbvoprab2vw  36997  cbvoprab1davw  37030  cbvoprab2davw  37031  cbvoprab12davw  37034  bj-inftyexpitaudisj  38094  rfovcnvf1od  44963  oppcup3lem  50258  tposcurf2val  50353  oppcthinendcALT  50493  concom  50715