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

Theorem opeq2d 4342
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 4336 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  cop 4131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132
This theorem is referenced by:  fmptsng  6317  fmptsnd  6318  tfrlem11  7349  seqomlem0  7409  seqomlem1  7410  seqomlem4  7413  seqomeq12  7414  fundmen  7894  unxpdomlem1  8027  mulcanenq  9639  elreal2  9810  om2uzrdg  12575  uzrdgsuci  12579  seqeq2  12625  seqeq3  12626  s1val  13180  s1eq  13182  swrdlsw  13253  swrdccatwrd  13269  ccats1swrdeq  13270  ccatopth  13271  swrdccat  13293  swrdccat3blem  13295  swrdccat3b  13296  swrdccatin12d  13301  splval  13302  splcl  13303  cshfn  13336  cshw0  13340  cshwmodn  13341  repswcshw  13358  swrds2  13482  swrd2lsw  13492  eucalgval  15082  setsidvald  15670  ressval  15703  ressress  15714  prdsval  15887  imasval  15943  imasaddvallem  15961  cidval  16110  iscatd2  16114  oppcval  16145  ismon  16165  rescval  16259  idfucl  16313  funcres  16328  fucval  16390  fucpropd  16409  setcval  16499  catcval  16518  estrcval  16536  xpcval  16589  1stfcl  16609  2ndfcl  16610  curf12  16639  curf2val  16642  curfcl  16644  hofcl  16671  oduval  16902  ipoval  16926  frmdval  17160  oppgval  17549  symgval  17571  efgmval  17897  efgmnvl  17899  efgi  17904  frgpup3lem  17962  dprd2da  18213  dmdprdpr  18220  dprdpr  18221  pgpfaclem1  18252  mgpval  18264  mgpress  18272  opprval  18396  sraval  18946  rlmval2  18964  psrval  19132  opsrval  19244  opsrval2  19246  zlmval  19631  znval  19650  znval2  19652  thlval  19806  islindf4  19944  matval  19984  mat1dimmul  20049  mat1dimcrng  20050  mat1scmat  20112  mdet0pr  20165  m1detdiag  20170  txkgen  21213  pt1hmeo  21367  xpstopnlem1  21370  tusval  21828  tmsval  22044  tngval  22201  om1val  22586  pi1xfrcnvlem  22612  pi1xfrcnv  22613  dchrval  24704  ttgval  25501  eengv  25605  wwlkextwrd  26050  wwlkextproplem3  26065  clwlkisclwwlk2  26112  clwwlkf1  26118  clwlkfoclwwlk  26166  clwlkf1clwwlklem  26170  clwlkf1clwwlk  26171  clwlksizeeq  26173  eupath2lem3  26300  numclwlk1lem2f1  26415  numclwlk2lem2f1o  26426  br8d  28596  resvval  28952  smatfval  28983  smatrcl  28984  smatlem  28985  fvproj  29021  qqhval  29140  iwrdsplit  29570  bnj66  29978  bnj1234  30129  bnj1296  30137  bnj1450  30166  bnj1463  30171  bnj1501  30183  bnj1523  30187  subfacp1lem5  30214  cvmliftlem10  30324  cvmlift2lem12  30344  msubffval  30468  msubfval  30469  elmsubrn  30473  msubrn  30474  msubco  30476  br8  30693  br6  30694  btwnouttr2  31093  brfs  31150  btwnconn1lem11  31168  csbfinxpg  32195  finixpnum  32358  ldualset  33224  tgrpfset  34844  tgrpset  34845  erngfset  34899  erngset  34900  erngfset-rN  34907  erngset-rN  34908  dvafset  35104  dvaset  35105  dvhfset  35181  dvhset  35182  dvhfvadd  35192  dvhopvadd2  35195  dib1dim2  35269  dicvscacl  35292  cdlemn6  35303  dihopelvalcpre  35349  dih1dimatlem  35430  hdmapfval  35931  hlhilset  36038  mendval  36566  ovolval4lem1  39333  ovolval4lem2  39334  ovnovollem3  39342  pfxpfx  40073  pfxccatin12d  40090  funopsn  40134  uspgr1ewop  40466  usgr2v1e2w  40470  1loopgruspgr  40707  1egrvtxdg1r  40718  1egrvtxdg0  40719  wwlksnextwrd  41095  wwlksnextproplem3  41109  clwlkclwwlk2  41204  clwwlksf1  41216  clwlksfoclwwlk  41262  clwlksf1clwwlklem  41267  clwlksf1clwwlk  41268  clwlkssizeeq  41270  eupth2lem3lem3  41390  eupth2  41399  av-numclwlk1lem2f1  41516  av-numclwlk2lem2f1o  41527  idfusubc0  41647  idfusubc  41648  rngcvalALTV  41745  ringcvalALTV  41791  zlmodzxzsub  41923  lmod1zr  42068
  Copyright terms: Public domain W3C validator