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

Theorem opeq1d 4546
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 4540 . 2 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  cop 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324
This theorem is referenced by:  oteq1  4549  oteq2  4550  opth  5073  elsnxp  5822  cbvoprab2  6876  unxpdomlem1  8321  djulf1o  8939  djurf1o  8940  mulcanenq  9985  ax1rid  10185  axrnegex  10186  fseq1m1p1  12623  uzrdglem  12965  swrd0swrd  13671  swrdccat  13703  swrdccat3a  13704  swrdccat3blem  13705  cshw0  13750  cshwmodn  13751  s2prop  13862  s4prop  13865  fsum2dlem  14710  fprod2dlem  14918  ruclem1  15167  imasaddvallem  16398  iscatd2  16550  moni  16604  homadmcd  16900  curf1  17074  curf1cl  17077  curf2  17078  hofcl  17108  gsum2dlem2  18578  imasdsf1olem  22399  ovoliunlem1  23491  cxpcn3  24711  axlowdimlem15  26058  axlowdim  26063  nvi  27810  nvop  27872  phop  28014  br8d  29761  fgreu  29812  1stpreimas  29824  smatfval  30202  smatrcl  30203  smatlem  30204  fvproj  30240  mvhfval  31769  mpst123  31776  br8  31985  nosupbnd2  32200  fvtransport  32477  rfovcnvf1od  38825
  Copyright terms: Public domain W3C validator