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

Theorem opeq2d 4400
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 4394 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  cop 4174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175
This theorem is referenced by:  funopsn  6398  fmptsng  6419  fmptsnd  6420  tfrlem11  7469  seqomlem0  7529  seqomlem1  7530  seqomlem4  7533  seqomeq12  7534  fundmen  8015  unxpdomlem1  8149  mulcanenq  9767  elreal2  9938  om2uzrdg  12738  uzrdgsuci  12742  seqeq2  12788  seqeq3  12789  s1val  13361  s1eq  13363  swrdlsw  13434  swrdccatwrd  13450  ccats1swrdeq  13451  ccatopth  13452  swrdccat  13474  swrdccat3blem  13476  swrdccat3b  13477  swrdccatin12d  13482  splval  13483  splcl  13484  cshfn  13517  cshw0  13521  cshwmodn  13522  repswcshw  13539  swrds2  13666  swrd2lsw  13676  eucalgval  15276  setsidvald  15870  ressval  15908  ressress  15919  prdsval  16096  imasval  16152  imasaddvallem  16170  cidval  16319  iscatd2  16323  oppcval  16354  ismon  16374  rescval  16468  idfucl  16522  funcres  16537  fucval  16599  fucpropd  16618  setcval  16708  catcval  16727  estrcval  16745  xpcval  16798  1stfcl  16818  2ndfcl  16819  curf12  16848  curf2val  16851  curfcl  16853  hofcl  16880  oduval  17111  ipoval  17135  frmdval  17369  oppgval  17758  symgval  17780  efgmval  18106  efgmnvl  18108  efgi  18113  frgpup3lem  18171  dprd2da  18422  dmdprdpr  18429  dprdpr  18430  pgpfaclem1  18461  mgpval  18473  mgpress  18481  opprval  18605  sraval  19157  rlmval2  19175  psrval  19343  opsrval  19455  opsrval2  19457  zlmval  19845  znval  19864  znval2  19866  thlval  20020  islindf4  20158  matval  20198  mat1dimmul  20263  mat1dimcrng  20264  mat1scmat  20326  mdet0pr  20379  m1detdiag  20384  txkgen  21436  pt1hmeo  21590  xpstopnlem1  21593  tusval  22051  tmsval  22267  tngval  22424  om1val  22811  pi1xfrcnvlem  22837  pi1xfrcnv  22838  dchrval  24940  ttgval  25736  eengv  25840  uspgr1ewop  26121  usgr2v1e2w  26125  1loopgruspgr  26377  1egrvtxdg1r  26387  1egrvtxdg0  26388  wwlksnextwrd  26773  wwlksnextproplem3  26787  clwlkclwwlk2  26885  clwwlksf1  26897  clwlksfoclwwlk  26943  clwlksf1clwwlklem  26948  clwlksf1clwwlk  26949  clwlkssizeeq  26951  eupth2lem3lem3  27070  eupth2  27079  numclwlk1lem2f1  27198  numclwlk2lem2f1o  27209  br8d  29394  resvval  29801  smatfval  29835  smatrcl  29836  smatlem  29837  fvproj  29873  qqhval  29992  iwrdsplit  30423  bnj66  30904  bnj1234  31055  bnj1296  31063  bnj1450  31092  bnj1463  31097  bnj1501  31109  bnj1523  31113  subfacp1lem5  31140  cvmliftlem10  31250  cvmlift2lem12  31270  msubffval  31394  msubfval  31395  elmsubrn  31399  msubrn  31400  msubco  31402  br8  31621  br6  31622  nosupbnd2lem1  31835  btwnouttr2  32104  brfs  32161  btwnconn1lem11  32179  csbfinxpg  33196  finixpnum  33365  ldualset  34231  tgrpfset  35851  tgrpset  35852  erngfset  35906  erngset  35907  erngfset-rN  35914  erngset-rN  35915  dvafset  36111  dvaset  36112  dvhfset  36188  dvhset  36189  dvhfvadd  36199  dvhopvadd2  36202  dib1dim2  36276  dicvscacl  36299  cdlemn6  36310  dihopelvalcpre  36356  dih1dimatlem  36437  hdmapfval  36938  hlhilset  37045  mendval  37572  ovolval4lem1  40626  ovolval4lem2  40627  ovnovollem3  40635  pfxpfx  41180  pfxccatin12d  41197  idfusubc0  41630  idfusubc  41631  rngcvalALTV  41726  ringcvalALTV  41772  zlmodzxzsub  41903  lmod1zr  42047
  Copyright terms: Public domain W3C validator