Theorem opeq2d 4812

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

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  dfid2  5492  funopsn  7029  fmptsng  7049  fmptsnd  7050  fvproj  7984  tfrlem11  8228  seqomlem0  8289  seqomlem1  8290  seqomlem4  8293  seqomeq12  8294  fundmen  8830  dif1en  8954  unxpdomlem1  9036  mulcanenq  10725  elreal2  10897  om2uzrdg  13685  uzrdgsuci  13689  seqeq2  13734  seqeq3  13735  s1val  14312  s1eq  14314  swrdlsw  14389  pfxpfx  14430  swrdccat  14457  swrdccat3blem  14461  swrdccat3b  14462  pfxccatin12d  14467  swrds2  14662  swrds2m  14663  swrd2lsw  14674  eucalgval  16296  setsidvald  16909  setsidvaldOLD  16910  ressval  16953  ressress  16967  prdsval  17175  imasval  17231  imasaddvallem  17249  xpsfval  17286  xpsval  17290  cidval  17395  iscatd2  17399  oppcval  17431  ismon  17454  rescval  17548  idfucl  17605  funcres  17620  fucval  17684  fucpropd  17704  setcval  17801  catcval  17824  estrcval  17849  xpcval  17903  1stfcl  17923  2ndfcl  17924  curf12  17954  curf2val  17957  curfcl  17959  hofcl  17986  oduval  18015  ipoval  18257  frmdval  18499  efmnd  18518  oppgval  18960  symgvalstruct  19013  symgvalstructOLD  19014  efgmval  19327  efgmnvl  19329  efgi  19334  frgpup3lem  19392  dprd2da  19654  dmdprdpr  19661  dprdpr  19662  pgpfaclem1  19693  mgpval  19732  mgpress  19744  mgpressOLD  19745  opprval  19872  sraval  20447  rlmval2  20473  zlmval  20726  znval  20748  znval2  20750  thlval  20909  islindf4  21054  psrval  21127  opsrval  21256  opsrval2  21258  matval  21567  mat1dimmul  21634  mat1dimcrng  21635  mat1scmat  21697  mdet0pr  21750  m1detdiag  21755  txkgen  22812  pt1hmeo  22966  xpstopnlem1  22969  xpstopnlem2  22971  tusval  23426  tmsval  23645  tngval  23804  om1val  24202  pi1xfrcnvlem  24228  pi1xfrcnv  24229  dchrval  26391  ttgval  27245  ttgvalOLD  27246  eengv  27356  uspgr1ewop  27624  usgr2v1e2w  27628  1loopgruspgr  27876  1egrvtxdg1r  27886  1egrvtxdg0  27887  eupth2lem3lem3  28603  eupth2  28612  wlkl0  28740  br8d  30959  resvval  31535  idlsrgval  31657  smatfval  31754  smatrcl  31755  smatlem  31756  qqhval  31933  bnj66  32849  bnj1234  33002  bnj1296  33010  bnj1450  33039  bnj1463  33044  bnj1501  33056  bnj1523  33060  subfacp1lem5  33155  cvmliftlem10  33265  cvmlift2lem12  33285  goaleq12d  33322  sategoelfvb  33390  msubffval  33494  msubfval  33495  elmsubrn  33499  msubrn  33500  msubco  33502  br8  33732  br6  33733  nosupbnd2lem1  33927  noinfbnd2lem1  33942  btwnouttr2  34333  brfs  34390  btwnconn1lem11  34408  bj-dfid2ALT  35245  bj-endval  35495  csbfinxpg  35568  finixpnum  35771  ldualset  37146  tgrpfset  38765  tgrpset  38766  erngfset  38820  erngset  38821  erngfset-rN  38828  erngset-rN  38829  dvafset  39025  dvaset  39026  dvhfset  39101  dvhset  39102  dvhfvadd  39112  dvhopvadd2  39115  dib1dim2  39189  dicvscacl  39212  cdlemn6  39223  dihopelvalcpre  39269  dih1dimatlem  39350  hdmapfval  39848  hlhilset  39955  mendval  41015  mnringvald  41833  ovolval4lem1  44194  ovolval4lem2  44195  ovnovollem3  44203  idfusubc0  45434  idfusubc  45435  rngcvalALTV  45530  ringcvalALTV  45576  zlmodzxzsub  45707  lmod1zr  45845  2arymaptf  46009  prstcval  46356  mndtcval  46377