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 3900  df-un 3902  df-ss 3915  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  6295  cbvoprab2  7509  cbvoprab12v  7511  fvproj  8152  unxpdomlem1  9248  djulf1o  9994  djurf1o  9995  mulcanenq  11046  ax1rid  11247  axrnegex  11248  fseq1m1p1  13734  uzrdglem  14101  pfxswrd  14856  swrdccat  14885  swrdccat3blem  14889  cshw0  14946  cshwmodn  14947  s2prop  15059  s4prop  15062  fsum2dlem  15937  fprod2dlem  16148  ruclem1  16400  imasaddvallem  17702  iscatd2  17856  moni  17912  homadmcd  18218  curf1  18400  curf1cl  18403  curf2  18404  hofcl  18434  gsum2dlem2  20186  pzriprnglem10  21797  imasdsf1olem  24693  ovoliunlem1  25824  cxpcn3  27077  nosupbnd2  28074  noinfbnd2  28089  noseqrdglem  28692  axlowdimlem15  29535  axlowdim  29540  nvi  31217  nvop  31279  phop  31421  br8d  33203  fgreu  33266  1stpreimas  33300  rlocval  33821  rloccring  33833  smatfval  34428  smatrcl  34429  smatlem  34430  fmla0xp  36149  mvhfval  36299  mpst123  36306  br8  36522  fvtransport  36798  cbvoprab1vw  37027  cbvoprab2vw  37028  cbvoprab1davw  37061  cbvoprab2davw  37062  cbvoprab12davw  37065  bj-inftyexpitaudisj  38128  rfovcnvf1od  45005  oppcup3lem  50315  tposcurf2val  50410  oppcthinendcALT  50550  concom  50772