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

Theorem opeq1d 4202
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 4196 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1468  cop 4001
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002
This theorem is referenced by:  oteq1  4205  oteq2  4206  opth  4717  cbvoprab2  6439  unxpdomlem1  7860  mulcanenq  9470  ax1rid  9670  axrnegex  9671  fseq1m1p1  11967  uzrdglem  12284  swrd0swrd  12951  swrdccat  12982  swrdccat3a  12983  swrdccat3blem  12984  cshw0  13029  cshwmodn  13030  s2prop  13140  s4prop  13143  fsum2dlem  13991  fprod2dlem  14194  ruclem1  14443  imasaddvallem  15600  iscatd2  15753  moni  15807  homadmcd  16103  curf1  16276  curf1cl  16279  curf2  16280  hofcl  16310  gsum2dlem2  17764  imasdsf1olem  21546  ovoliunlem1  22614  cxpcn3  23849  axlowdimlem15  25147  axlowdim  25152  nvi  26396  nvop  26469  phop  26622  br8d  28376  fgreu  28431  1stpreimas  28443  smatfval  28776  smatrcl  28777  smatlem  28778  fvproj  28814  mvhfval  30323  mpst123  30330  br8  30547  fvtransport  30950  rfovcnvf1od  36839
  Copyright terms: Public domain W3C validator