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

Theorem opeq2d 4440
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 4434 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cop 4216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217
This theorem is referenced by:  funopsn  6453  fmptsng  6475  fmptsnd  6476  tfrlem11  7529  seqomlem0  7589  seqomlem1  7590  seqomlem4  7593  seqomeq12  7594  fundmen  8071  unxpdomlem1  8205  mulcanenq  9820  elreal2  9991  om2uzrdg  12795  uzrdgsuci  12799  seqeq2  12845  seqeq3  12846  s1val  13414  s1eq  13416  swrdlsw  13498  swrdccatwrd  13514  ccats1swrdeq  13515  ccatopth  13516  swrdccat  13539  swrdccat3blem  13541  swrdccat3b  13542  swrdccatin12d  13547  splval  13548  splcl  13549  cshfn  13582  cshw0  13586  cshwmodn  13587  repswcshw  13604  swrds2  13731  swrd2lsw  13741  eucalgval  15342  setsidvald  15936  ressval  15974  ressress  15985  prdsval  16162  imasval  16218  imasaddvallem  16236  cidval  16385  iscatd2  16389  oppcval  16420  ismon  16440  rescval  16534  idfucl  16588  funcres  16603  fucval  16665  fucpropd  16684  setcval  16774  catcval  16793  estrcval  16811  xpcval  16864  1stfcl  16884  2ndfcl  16885  curf12  16914  curf2val  16917  curfcl  16919  hofcl  16946  oduval  17177  ipoval  17201  frmdval  17435  oppgval  17823  symgval  17845  efgmval  18171  efgmnvl  18173  efgi  18178  frgpup3lem  18236  dprd2da  18487  dmdprdpr  18494  dprdpr  18495  pgpfaclem1  18526  mgpval  18538  mgpress  18546  opprval  18670  sraval  19224  rlmval2  19242  psrval  19410  opsrval  19522  opsrval2  19524  zlmval  19912  znval  19931  znval2  19933  thlval  20087  islindf4  20225  matval  20265  mat1dimmul  20330  mat1dimcrng  20331  mat1scmat  20393  mdet0pr  20446  m1detdiag  20451  txkgen  21503  pt1hmeo  21657  xpstopnlem1  21660  tusval  22117  tmsval  22333  tngval  22490  om1val  22876  pi1xfrcnvlem  22902  pi1xfrcnv  22903  dchrval  25004  ttgval  25800  eengv  25904  uspgr1ewop  26185  usgr2v1e2w  26189  1loopgruspgr  26452  1egrvtxdg1r  26462  1egrvtxdg0  26463  wwlksnextwrd  26860  wwlksnextproplem3  26874  clwlkclwwlk2  26969  clwwlkf1  27012  clwlksfoclwwlk  27050  clwlksf1clwwlklem  27055  clwlksf1clwwlk  27056  clwlkssizeeq  27058  eupth2lem3lem3  27208  eupth2  27217  numclwlk1lem2f1  27347  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  br8d  29548  resvval  29955  smatfval  29989  smatrcl  29990  smatlem  29991  fvproj  30027  qqhval  30146  iwrdsplit  30577  bnj66  31056  bnj1234  31207  bnj1296  31215  bnj1450  31244  bnj1463  31249  bnj1501  31261  bnj1523  31265  subfacp1lem5  31292  cvmliftlem10  31402  cvmlift2lem12  31422  msubffval  31546  msubfval  31547  elmsubrn  31551  msubrn  31552  msubco  31554  br8  31772  br6  31773  nosupbnd2lem1  31986  btwnouttr2  32254  brfs  32311  btwnconn1lem11  32329  csbfinxpg  33355  finixpnum  33524  ldualset  34730  tgrpfset  36349  tgrpset  36350  erngfset  36404  erngset  36405  erngfset-rN  36412  erngset-rN  36413  dvafset  36609  dvaset  36610  dvhfset  36686  dvhset  36687  dvhfvadd  36697  dvhopvadd2  36700  dib1dim2  36774  dicvscacl  36797  cdlemn6  36808  dihopelvalcpre  36854  dih1dimatlem  36935  hdmapfval  37436  hlhilset  37543  mendval  38070  ovolval4lem1  41184  ovolval4lem2  41185  ovnovollem3  41193  pfxpfx  41740  pfxccatin12d  41757  idfusubc0  42190  idfusubc  42191  rngcvalALTV  42286  ringcvalALTV  42332  zlmodzxzsub  42463  lmod1zr  42607
  Copyright terms: Public domain W3C validator