MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq1d Structured version   Visualization version   GIF version

Theorem opeq1d 4340
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
StepHypRef Expression
1 opeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opeq1 4334 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cop 4130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131
This theorem is referenced by:  oteq1  4343  oteq2  4344  opth  4865  elsnxp  5580  cbvoprab2  6604  unxpdomlem1  8026  mulcanenq  9638  ax1rid  9838  axrnegex  9839  fseq1m1p1  12239  uzrdglem  12573  swrd0swrd  13259  swrdccat  13290  swrdccat3a  13291  swrdccat3blem  13292  cshw0  13337  cshwmodn  13338  s2prop  13448  s4prop  13451  fsum2dlem  14289  fprod2dlem  14495  ruclem1  14745  imasaddvallem  15958  iscatd2  16111  moni  16165  homadmcd  16461  curf1  16634  curf1cl  16637  curf2  16638  hofcl  16668  gsum2dlem2  18139  imasdsf1olem  21929  ovoliunlem1  22994  cxpcn3  24206  axlowdimlem15  25554  axlowdim  25559  nvi  26637  nvop  26710  phop  26863  br8d  28608  fgreu  28660  1stpreimas  28672  smatfval  28995  smatrcl  28996  smatlem  28997  fvproj  29033  mvhfval  30490  mpst123  30497  br8  30705  fvtransport  31115  rfovcnvf1od  37121
  Copyright terms: Public domain W3C validator