Theorem opeq2d 4347

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

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq2 4341	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

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:  funopsn  6319  fmptsng  6339  fmptsnd  6340  tfrlem11  7371  seqomlem0  7431  seqomlem1  7432  seqomlem4  7435  seqomeq12  7436  fundmen  7916  unxpdomlem1  8049  mulcanenq  9661  elreal2  9832  om2uzrdg  12617  uzrdgsuci  12621  seqeq2  12667  seqeq3  12668  s1val  13231  s1eq  13233  swrdlsw  13304  swrdccatwrd  13320  ccats1swrdeq  13321  ccatopth  13322  swrdccat  13344  swrdccat3blem  13346  swrdccat3b  13347  swrdccatin12d  13352  splval  13353  splcl  13354  cshfn  13387  cshw0  13391  cshwmodn  13392  repswcshw  13409  swrds2  13533  swrd2lsw  13543  eucalgval  15133  setsidvald  15721  ressval  15754  ressress  15765  prdsval  15938  imasval  15994  imasaddvallem  16012  cidval  16161  iscatd2  16165  oppcval  16196  ismon  16216  rescval  16310  idfucl  16364  funcres  16379  fucval  16441  fucpropd  16460  setcval  16550  catcval  16569  estrcval  16587  xpcval  16640  1stfcl  16660  2ndfcl  16661  curf12  16690  curf2val  16693  curfcl  16695  hofcl  16722  oduval  16953  ipoval  16977  frmdval  17211  oppgval  17600  symgval  17622  efgmval  17948  efgmnvl  17950  efgi  17955  frgpup3lem  18013  dprd2da  18264  dmdprdpr  18271  dprdpr  18272  pgpfaclem1  18303  mgpval  18315  mgpress  18323  opprval  18447  sraval  18997  rlmval2  19015  psrval  19183  opsrval  19295  opsrval2  19297  zlmval  19683  znval  19702  znval2  19704  thlval  19858  islindf4  19996  matval  20036  mat1dimmul  20101  mat1dimcrng  20102  mat1scmat  20164  mdet0pr  20217  m1detdiag  20222  txkgen  21265  pt1hmeo  21419  xpstopnlem1  21422  tusval  21880  tmsval  22096  tngval  22253  om1val  22638  pi1xfrcnvlem  22664  pi1xfrcnv  22665  dchrval  24759  ttgval  25555  eengv  25659  wwlkextwrd  26256  wwlkextproplem3  26271  clwlkisclwwlk2  26318  clwwlkf1  26324  clwlkfoclwwlk  26372  clwlkf1clwwlklem  26376  clwlkf1clwwlk  26377  clwlksizeeq  26379  eupath2lem3  26506  numclwlk1lem2f1  26621  numclwlk2lem2f1o  26632  br8d  28802  resvval  29158  smatfval  29189  smatrcl  29190  smatlem  29191  fvproj  29227  qqhval  29346  iwrdsplit  29776  bnj66  30184  bnj1234  30335  bnj1296  30343  bnj1450  30372  bnj1463  30377  bnj1501  30389  bnj1523  30393  subfacp1lem5  30420  cvmliftlem10  30530  cvmlift2lem12  30550  msubffval  30674  msubfval  30675  elmsubrn  30679  msubrn  30680  msubco  30682  br8  30899  br6  30900  btwnouttr2  31299  brfs  31356  btwnconn1lem11  31374  csbfinxpg  32401  finixpnum  32564  ldualset  33430  tgrpfset  35050  tgrpset  35051  erngfset  35105  erngset  35106  erngfset-rN  35113  erngset-rN  35114  dvafset  35310  dvaset  35311  dvhfset  35387  dvhset  35388  dvhfvadd  35398  dvhopvadd2  35401  dib1dim2  35475  dicvscacl  35498  cdlemn6  35509  dihopelvalcpre  35555  dih1dimatlem  35636  hdmapfval  36137  hlhilset  36244  mendval  36772  ovolval4lem1  39539  ovolval4lem2  39540  ovnovollem3  39548  pfxpfx  40278  pfxccatin12d  40295  uspgr1ewop  40474  usgr2v1e2w  40478  1loopgruspgr  40715  1egrvtxdg1r  40726  1egrvtxdg0  40727  wwlksnextwrd  41103  wwlksnextproplem3  41117  clwlkclwwlk2  41212  clwwlksf1  41224  clwlksfoclwwlk  41270  clwlksf1clwwlklem  41275  clwlksf1clwwlk  41276  clwlkssizeeq  41278  eupth2lem3lem3  41398  eupth2  41407  av-numclwlk1lem2f1  41524  av-numclwlk2lem2f1o  41535  idfusubc0  41655  idfusubc  41656  rngcvalALTV  41753  ringcvalALTV  41799  zlmodzxzsub  41931  lmod1zr  42076