Theorem opeq2d 4684

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

Syntax hints:   → wi 4   = wceq 1507  ⟨cop 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-rab 3098  df-v 3418  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-nul 4180  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448

This theorem is referenced by:  funopsn  6733  fmptsng  6753  fmptsnd  6754  tfrlem11  7828  seqomlem0  7888  seqomlem1  7889  seqomlem4  7892  seqomeq12  7893  fundmen  8380  unxpdomlem1  8517  mulcanenq  10180  elreal2  10352  om2uzrdg  13139  uzrdgsuci  13143  seqeq2  13188  seqeq3  13189  s1val  13761  s1eq  13763  swrdlsw  13845  pfxpfx  13893  swrdccatwrdOLD  13903  ccats1swrdeqOLD  13905  ccatopthOLD  13908  swrdccat  13938  swrdccatOLD  13939  swrdccat3blem  13944  swrdccat3b  13945  swrdccat3bOLD  13946  pfxccatin12d  13953  swrdccatin12dOLD  13954  splvalpfxOLD  13962  splvalOLD  13964  splclOLD  13966  cshfnOLD  14012  swrds2  14164  swrds2m  14165  swrd2lsw  14176  eucalgval  15782  setsidvald  16370  ressval  16407  ressress  16418  prdsval  16584  imasval  16640  imasaddvallem  16658  cidval  16806  iscatd2  16810  oppcval  16841  ismon  16861  rescval  16955  idfucl  17009  funcres  17024  fucval  17086  fucpropd  17105  setcval  17195  catcval  17214  estrcval  17232  xpcval  17285  1stfcl  17305  2ndfcl  17306  curf12  17335  curf2val  17338  curfcl  17340  hofcl  17367  oduval  17598  ipoval  17622  frmdval  17857  oppgval  18246  symgval  18268  efgmval  18596  efgmnvl  18598  efgi  18603  frgpup3lem  18663  dprd2da  18914  dmdprdpr  18921  dprdpr  18922  pgpfaclem1  18953  mgpval  18965  mgpress  18973  opprval  19097  sraval  19670  rlmval2  19688  psrval  19856  opsrval  19968  opsrval2  19970  zlmval  20365  znval  20384  znval2  20386  thlval  20541  islindf4  20684  matval  20724  mat1dimmul  20789  mat1dimcrng  20790  mat1scmat  20852  mdet0pr  20905  m1detdiag  20910  txkgen  21964  pt1hmeo  22118  xpstopnlem1  22121  tusval  22578  tmsval  22794  tngval  22951  om1val  23337  pi1xfrcnvlem  23363  pi1xfrcnv  23364  dchrval  25512  ttgval  26364  eengv  26468  uspgr1ewop  26733  usgr2v1e2w  26737  1loopgruspgr  26985  1egrvtxdg1r  26995  1egrvtxdg0  26996  wwlksnextwrdOLD  27393  wwlksnextproplem3OLD  27414  clwlkclwwlk2OLD  27511  clwlkclwwlkfoOLD  27519  clwlkclwwlkf1OLD  27520  clwlkclwwlkenOLD  27527  clwwlkf1OLD  27566  clwlknf1oclwwlknOLD  27611  eupth2lem3lem3  27760  eupth2  27769  numclwwlk1lem2f1OLD  27904  wlkl0  27920  numclwlk2lem2f1oOLD  27935  br8d  30125  resvval  30576  smatfval  30699  smatrcl  30700  smatlem  30701  fvproj  30737  qqhval  30856  iwrdsplitOLD  31288  bnj66  31776  bnj1234  31927  bnj1296  31935  bnj1450  31964  bnj1463  31969  bnj1501  31981  bnj1523  31985  subfacp1lem5  32013  cvmliftlem10  32123  cvmlift2lem12  32143  goaleq12d  32177  msubffval  32287  msubfval  32288  elmsubrn  32292  msubrn  32293  msubco  32295  br8  32509  br6  32510  nosupbnd2lem1  32733  btwnouttr2  33001  brfs  33058  btwnconn1lem11  33076  csbfinxpg  34107  finixpnum  34315  ldualset  35703  tgrpfset  37322  tgrpset  37323  erngfset  37377  erngset  37378  erngfset-rN  37385  erngset-rN  37386  dvafset  37582  dvaset  37583  dvhfset  37658  dvhset  37659  dvhfvadd  37669  dvhopvadd2  37672  dib1dim2  37746  dicvscacl  37769  cdlemn6  37780  dihopelvalcpre  37826  dih1dimatlem  37907  hdmapfval  38405  hlhilset  38512  mendval  39176  ovolval4lem1  42360  ovolval4lem2  42361  ovnovollem3  42369  idfusubc0  43498  idfusubc  43499  rngcvalALTV  43594  ringcvalALTV  43640  zlmodzxzsub  43770  lmod1zr  43913