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

Theorem opeq2d 4602
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)
Hypothesis
Ref Expression
opeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
opeq2d (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2d
StepHypRef Expression
1 opeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opeq2 4596 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cop 4376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377
This theorem is referenced by:  funopsn  6633  fmptsng  6655  fmptsnd  6656  tfrlem11  7716  seqomlem0  7776  seqomlem1  7777  seqomlem4  7780  seqomeq12  7781  fundmen  8262  unxpdomlem1  8399  mulcanenq  10063  elreal2  10234  om2uzrdg  12975  uzrdgsuci  12979  seqeq2  13024  seqeq3  13025  s1val  13589  s1eq  13591  swrdlsw  13672  swrdccatwrd  13688  ccats1swrdeq  13689  ccatopth  13690  swrdccat  13713  swrdccat3blem  13715  swrdccat3b  13716  swrdccatin12d  13721  splval  13722  splcl  13723  cshfn  13756  cshw0  13760  cshwmodn  13761  repswcshw  13778  swrds2  13905  swrds2m  13906  swrd2lsw  13916  eucalgval  15510  setsidvald  16096  ressval  16134  ressress  16146  prdsval  16316  imasval  16372  imasaddvallem  16390  cidval  16538  iscatd2  16542  oppcval  16573  ismon  16593  rescval  16687  idfucl  16741  funcres  16756  fucval  16818  fucpropd  16837  setcval  16927  catcval  16946  estrcval  16964  xpcval  17018  1stfcl  17038  2ndfcl  17039  curf12  17068  curf2val  17071  curfcl  17073  hofcl  17100  oduval  17331  ipoval  17355  frmdval  17589  oppgval  17974  symgval  17996  efgmval  18322  efgmnvl  18324  efgi  18329  frgpup3lem  18387  dprd2da  18639  dmdprdpr  18646  dprdpr  18647  pgpfaclem1  18678  mgpval  18690  mgpress  18698  opprval  18822  sraval  19381  rlmval2  19399  psrval  19567  opsrval  19679  opsrval2  19681  zlmval  20068  znval  20087  znval2  20089  thlval  20246  islindf4  20384  matval  20424  mat1dimmul  20490  mat1dimcrng  20491  mat1scmat  20553  mdet0pr  20606  m1detdiag  20611  txkgen  21666  pt1hmeo  21820  xpstopnlem1  21823  tusval  22280  tmsval  22496  tngval  22653  om1val  23039  pi1xfrcnvlem  23065  pi1xfrcnv  23066  dchrval  25172  ttgval  25968  eengv  26072  uspgr1ewop  26355  usgr2v1e2w  26359  1loopgruspgr  26623  1egrvtxdg1r  26633  1egrvtxdg0  26634  wwlksnextwrd  27033  wwlksnextproplem3  27048  clwlkclwwlk2  27145  clwlkclwwlkfo  27151  clwlkclwwlkf1  27152  clwlkclwwlken  27154  clwwlkf1  27197  clwlksfoclwwlkOLD  27236  clwlksf1clwwlklemOLD  27241  clwlksf1clwwlkOLD  27242  clwlknf1oclwwlkn  27247  clwlkssizeeqOLD  27249  eupth2lem3lem3  27402  eupth2  27411  numclwwlk1lem2f1  27535  wlkl0  27546  numclwlk2lem2f1o  27558  numclwlk2lem2f1oOLD  27565  br8d  29746  resvval  30151  smatfval  30185  smatrcl  30186  smatlem  30187  fvproj  30223  qqhval  30342  iwrdsplit  30773  bnj66  31251  bnj1234  31402  bnj1296  31410  bnj1450  31439  bnj1463  31444  bnj1501  31456  bnj1523  31460  subfacp1lem5  31487  cvmliftlem10  31597  cvmlift2lem12  31617  msubffval  31741  msubfval  31742  elmsubrn  31746  msubrn  31747  msubco  31749  br8  31966  br6  31967  nosupbnd2lem1  32180  btwnouttr2  32448  brfs  32505  btwnconn1lem11  32523  csbfinxpg  33539  finixpnum  33705  ldualset  34903  tgrpfset  36522  tgrpset  36523  erngfset  36577  erngset  36578  erngfset-rN  36585  erngset-rN  36586  dvafset  36782  dvaset  36783  dvhfset  36858  dvhset  36859  dvhfvadd  36869  dvhopvadd2  36872  dib1dim2  36946  dicvscacl  36969  cdlemn6  36980  dihopelvalcpre  37026  dih1dimatlem  37107  hdmapfval  37605  hlhilset  37712  mendval  38251  ovolval4lem1  41342  ovolval4lem2  41343  ovnovollem3  41351  pfxpfx  41987  pfxccatin12d  42004  idfusubc0  42430  idfusubc  42431  rngcvalALTV  42526  ringcvalALTV  42572  zlmodzxzsub  42703  lmod1zr  42847
  Copyright terms: Public domain W3C validator