Theorem opeq2d 4842

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 4836	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598

This theorem is referenced by:  dfid2  5538  funopsn  7099  fmptsng  7119  fmptsnd  7120  fvproj  8071  tfrlem11  8339  seqomlem0  8400  seqomlem1  8401  seqomlem4  8404  seqomeq12  8405  fundmen  8982  dif1en  9111  dif1enOLD  9113  unxpdomlem1  9201  mulcanenq  10905  elreal2  11077  om2uzrdg  13871  uzrdgsuci  13875  seqeq2  13920  seqeq3  13921  s1val  14498  s1eq  14500  swrdlsw  14567  pfxpfx  14608  swrdccat  14635  swrdccat3blem  14639  swrdccat3b  14640  pfxccatin12d  14645  swrds2  14841  swrds2m  14842  swrd2lsw  14853  eucalgval  16469  setsidvald  17082  setsidvaldOLD  17083  ressval  17126  ressress  17143  prdsval  17351  imasval  17407  imasaddvallem  17425  xpsfval  17462  xpsval  17466  cidval  17571  iscatd2  17575  oppcval  17607  ismon  17630  rescval  17724  idfucl  17781  funcres  17796  fucval  17860  fucpropd  17880  setcval  17977  catcval  18000  estrcval  18025  xpcval  18079  1stfcl  18099  2ndfcl  18100  curf12  18130  curf2val  18133  curfcl  18135  hofcl  18162  oduval  18191  ipoval  18433  frmdval  18675  efmnd  18694  oppgval  19139  symgvalstruct  19192  symgvalstructOLD  19193  efgmval  19508  efgmnvl  19510  efgi  19515  frgpup3lem  19573  dprd2da  19835  dmdprdpr  19842  dprdpr  19843  pgpfaclem1  19874  mgpval  19913  mgpress  19925  mgpressOLD  19926  opprval  20064  sraval  20696  rlmval2  20722  zlmval  20953  znval  20975  znval2  20977  thlval  21136  islindf4  21281  psrval  21354  opsrval  21484  opsrval2  21486  matval  21795  mat1dimmul  21862  mat1dimcrng  21863  mat1scmat  21925  mdet0pr  21978  m1detdiag  21983  txkgen  23040  pt1hmeo  23194  xpstopnlem1  23197  xpstopnlem2  23199  tusval  23654  tmsval  23873  tngval  24032  om1val  24430  pi1xfrcnvlem  24456  pi1xfrcnv  24457  dchrval  26619  nosupbnd2lem1  27100  noinfbnd2lem1  27115  ttgval  27880  ttgvalOLD  27881  eengv  27991  uspgr1ewop  28259  usgr2v1e2w  28263  1loopgruspgr  28511  1egrvtxdg1r  28521  1egrvtxdg0  28522  eupth2lem3lem3  29237  eupth2  29246  wlkl0  29374  br8d  31596  resvval  32189  idlsrgval  32321  smatfval  32465  smatrcl  32466  smatlem  32467  qqhval  32644  bnj66  33561  bnj1234  33714  bnj1296  33722  bnj1450  33751  bnj1463  33756  bnj1501  33768  bnj1523  33772  subfacp1lem5  33865  cvmliftlem10  33975  cvmlift2lem12  33995  goaleq12d  34032  sategoelfvb  34100  msubffval  34204  msubfval  34205  elmsubrn  34209  msubrn  34210  msubco  34212  br8  34415  br6  34416  btwnouttr2  34683  brfs  34740  btwnconn1lem11  34758  bj-dfid2ALT  35609  bj-endval  35859  csbfinxpg  35932  finixpnum  36136  ldualset  37660  tgrpfset  39280  tgrpset  39281  erngfset  39335  erngset  39336  erngfset-rN  39343  erngset-rN  39344  dvafset  39540  dvaset  39541  dvhfset  39616  dvhset  39617  dvhfvadd  39627  dvhopvadd2  39630  dib1dim2  39704  dicvscacl  39727  cdlemn6  39738  dihopelvalcpre  39784  dih1dimatlem  39865  hdmapfval  40363  hlhilset  40470  mendval  41568  mnringvald  42591  ovolval4lem1  44991  ovolval4lem2  44992  ovnovollem3  45000  idfusubc0  46264  idfusubc  46265  rngcvalALTV  46360  ringcvalALTV  46406  zlmodzxzsub  46537  lmod1zr  46675  2arymaptf  46839  prstcval  47185  mndtcval  47206