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

Theorem opeq2d 4560
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 4554 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cop 4327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328
This theorem is referenced by:  funopsn  6577  fmptsng  6599  fmptsnd  6600  tfrlem11  7654  seqomlem0  7714  seqomlem1  7715  seqomlem4  7718  seqomeq12  7719  fundmen  8197  unxpdomlem1  8331  mulcanenq  9994  elreal2  10165  om2uzrdg  12969  uzrdgsuci  12973  seqeq2  13019  seqeq3  13020  s1val  13588  s1eq  13590  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  15517  setsidvald  16111  ressval  16149  ressress  16160  prdsval  16337  imasval  16393  imasaddvallem  16411  cidval  16559  iscatd2  16563  oppcval  16594  ismon  16614  rescval  16708  idfucl  16762  funcres  16777  fucval  16839  fucpropd  16858  setcval  16948  catcval  16967  estrcval  16985  xpcval  17038  1stfcl  17058  2ndfcl  17059  curf12  17088  curf2val  17091  curfcl  17093  hofcl  17120  oduval  17351  ipoval  17375  frmdval  17609  oppgval  17997  symgval  18019  efgmval  18345  efgmnvl  18347  efgi  18352  frgpup3lem  18410  dprd2da  18661  dmdprdpr  18668  dprdpr  18669  pgpfaclem1  18700  mgpval  18712  mgpress  18720  opprval  18844  sraval  19398  rlmval2  19416  psrval  19584  opsrval  19696  opsrval2  19698  zlmval  20086  znval  20105  znval2  20107  thlval  20261  islindf4  20399  matval  20439  mat1dimmul  20504  mat1dimcrng  20505  mat1scmat  20567  mdet0pr  20620  m1detdiag  20625  txkgen  21677  pt1hmeo  21831  xpstopnlem1  21834  tusval  22291  tmsval  22507  tngval  22664  om1val  23050  pi1xfrcnvlem  23076  pi1xfrcnv  23077  dchrval  25179  ttgval  25975  eengv  26079  uspgr1ewop  26360  usgr2v1e2w  26364  1loopgruspgr  26627  1egrvtxdg1r  26637  1egrvtxdg0  26638  wwlksnextwrd  27036  wwlksnextproplem3  27050  clwlkclwwlk2  27147  clwlkclwwlkfo  27153  clwlkclwwlkf1  27154  clwlkclwwlken  27156  clwwlkf1  27199  clwlksfoclwwlkOLD  27238  clwlksf1clwwlklemOLD  27243  clwlksf1clwwlkOLD  27244  clwlknf1oclwwlkn  27249  clwlkssizeeqOLD  27251  eupth2lem3lem3  27403  eupth2  27412  numclwlk1lem2f1  27537  wlkl0  27549  numclwlk2lem2f1o  27561  numclwlk2lem2f1oOLD  27568  br8d  29750  resvval  30157  smatfval  30191  smatrcl  30192  smatlem  30193  fvproj  30229  qqhval  30348  iwrdsplit  30779  bnj66  31258  bnj1234  31409  bnj1296  31417  bnj1450  31446  bnj1463  31451  bnj1501  31463  bnj1523  31467  subfacp1lem5  31494  cvmliftlem10  31604  cvmlift2lem12  31624  msubffval  31748  msubfval  31749  elmsubrn  31753  msubrn  31754  msubco  31756  br8  31974  br6  31975  nosupbnd2lem1  32188  btwnouttr2  32456  brfs  32513  btwnconn1lem11  32531  csbfinxpg  33554  finixpnum  33725  ldualset  34933  tgrpfset  36552  tgrpset  36553  erngfset  36607  erngset  36608  erngfset-rN  36615  erngset-rN  36616  dvafset  36812  dvaset  36813  dvhfset  36889  dvhset  36890  dvhfvadd  36900  dvhopvadd2  36903  dib1dim2  36977  dicvscacl  37000  cdlemn6  37011  dihopelvalcpre  37057  dih1dimatlem  37138  hdmapfval  37639  hlhilset  37746  mendval  38273  ovolval4lem1  41387  ovolval4lem2  41388  ovnovollem3  41396  pfxpfx  41943  pfxccatin12d  41960  idfusubc0  42393  idfusubc  42394  rngcvalALTV  42489  ringcvalALTV  42535  zlmodzxzsub  42666  lmod1zr  42810
  Copyright terms: Public domain W3C validator