Theorem opeq1d 4842

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594

This theorem is used by:  oteq1  4845  oteq2  4846  opth  5456  elsnxp  6293  cbvoprab2  7505  cbvoprab12v  7507  fvproj  8136  unxpdomlem1  9230  djulf1o  9921  djurf1o  9922  mulcanenq  10973  ax1rid  11174  axrnegex  11175  fseq1m1p1  13658  uzrdglem  14025  pfxswrd  14779  swrdccat  14808  swrdccat3blem  14812  cshw0  14869  cshwmodn  14870  s2prop  14982  s4prop  14985  fsum2dlem  15860  fprod2dlem  16073  ruclem1  16325  imasaddvallem  17621  iscatd2  17775  moni  17831  homadmcd  18137  curf1  18319  curf1cl  18322  curf2  18323  hofcl  18353  gsum2dlem2  20104  pzriprnglem10  21709  imasdsf1olem  24605  ovoliunlem1  25736  cxpcn3  26993  nosupbnd2  27960  noinfbnd2  27975  noseqrdglem  28578  axlowdimlem15  29421  axlowdim  29426  nvi  31103  nvop  31165  phop  31307  br8d  33089  fgreu  33152  1stpreimas  33186  rlocval  33707  rloccring  33719  smatfval  34313  smatrcl  34314  smatlem  34315  fmla0xp  35970  mvhfval  36120  mpst123  36127  br8  36343  fvtransport  36620  cbvoprab1vw  36865  cbvoprab2vw  36866  cbvoprab1davw  36899  cbvoprab2davw  36900  cbvoprab12davw  36903  bj-inftyexpitaudisj  37965  rfovcnvf1od  44852  oppcup3lem  50140  tposcurf2val  50235  oppcthinendcALT  50375  concom  50597