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

Theorem opeq1d 4244
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 4238 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cop 4034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
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 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035
This theorem is referenced by:  oteq1  4247  oteq2  4248  opth  4769  elsnxp  5484  cbvoprab2  6508  unxpdomlem1  7929  mulcanenq  9541  ax1rid  9741  axrnegex  9742  fseq1m1p1  12156  uzrdglem  12490  swrd0swrd  13176  swrdccat  13207  swrdccat3a  13208  swrdccat3blem  13209  cshw0  13254  cshwmodn  13255  s2prop  13365  s4prop  13368  fsum2dlem  14216  fprod2dlem  14422  ruclem1  14672  imasaddvallem  15908  iscatd2  16061  moni  16115  homadmcd  16411  curf1  16584  curf1cl  16587  curf2  16588  hofcl  16618  gsum2dlem2  18104  imasdsf1olem  21894  ovoliunlem1  22956  cxpcn3  24180  axlowdimlem15  25530  axlowdim  25535  nvi  26613  nvop  26686  phop  26839  br8d  28594  fgreu  28646  1stpreimas  28658  smatfval  28989  smatrcl  28990  smatlem  28991  fvproj  29027  mvhfval  30533  mpst123  30540  br8  30745  fvtransport  31148  rfovcnvf1od  37219
  Copyright terms: Public domain W3C validator