Theorem opeq2d 4904

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  dfid2  5595  funopsn  7182  fmptsng  7202  fmptsnd  7203  fvproj  8175  tfrlem11  8444  seqomlem0  8505  seqomlem1  8506  seqomlem4  8509  seqomeq12  8510  fundmen  9096  dif1en  9226  dif1enOLD  9228  unxpdomlem1  9313  mulcanenq  11029  elreal2  11201  om2uzrdg  14007  uzrdgsuci  14011  seqeq2  14056  seqeq3  14057  s1val  14646  s1eq  14648  swrdlsw  14715  pfxpfx  14756  swrdccat  14783  swrdccat3blem  14787  swrdccat3b  14788  pfxccatin12d  14793  swrds2  14989  swrds2m  14990  swrd2lsw  15001  eucalgval  16629  setsidvald  17246  setsidvaldOLD  17247  ressval  17290  ressress  17307  prdsval  17515  imasval  17571  imasaddvallem  17589  xpsfval  17626  xpsval  17630  cidval  17735  iscatd2  17739  oppcval  17771  ismon  17794  rescval  17888  idfucl  17945  funcres  17960  idfusubc0  17963  idfusubc  17964  fucval  18027  fucpropd  18047  setcval  18144  catcval  18167  estrcval  18192  xpcval  18246  1stfcl  18266  2ndfcl  18267  curf12  18297  curf2val  18300  curfcl  18302  hofcl  18329  oduval  18358  ipoval  18600  frmdval  18886  efmnd  18905  oppgval  19387  symgvalstruct  19438  symgvalstructOLD  19439  efgmval  19754  efgmnvl  19756  efgi  19761  frgpup3lem  19819  dprd2da  20086  dmdprdpr  20093  dprdpr  20094  pgpfaclem1  20125  mgpval  20164  mgpress  20176  mgpressOLD  20177  opprval  20361  sraval  21197  rlmval2  21222  pzriprnglem10  21524  zlmval  21549  znval  21573  znval2  21575  thlval  21736  islindf4  21881  psrval  21958  opsrval  22087  opsrval2  22089  matval  22436  mat1dimmul  22503  mat1dimcrng  22504  mat1scmat  22566  mdet0pr  22619  m1detdiag  22624  txkgen  23681  pt1hmeo  23835  xpstopnlem1  23838  xpstopnlem2  23840  tusval  24295  tmsval  24514  tngval  24673  om1val  25082  pi1xfrcnvlem  25108  pi1xfrcnv  25109  dchrval  27296  nosupbnd2lem1  27778  noinfbnd2lem1  27793  seqseq123d  28310  om2noseqrdg  28328  noseqrdgsuc  28332  ttgval  28901  ttgvalOLD  28902  eengv  29012  uspgr1ewop  29283  usgr2v1e2w  29287  1loopgruspgr  29536  1egrvtxdg1r  29546  1egrvtxdg0  29547  eupth2lem3lem3  30262  eupth2  30271  wlkl0  30399  br8d  32632  rlocval  33231  rlocf1  33245  resvval  33318  opprabs  33475  idlsrgval  33496  resssra  33602  smatfval  33741  smatrcl  33742  smatlem  33743  qqhval  33920  bnj66  34836  bnj1234  34989  bnj1296  34997  bnj1450  35026  bnj1463  35031  bnj1501  35043  bnj1523  35047  subfacp1lem5  35152  cvmliftlem10  35262  cvmlift2lem12  35282  goaleq12d  35319  sategoelfvb  35387  msubffval  35491  msubfval  35492  elmsubrn  35496  msubrn  35497  msubco  35499  br8  35718  br6  35719  btwnouttr2  35986  brfs  36043  btwnconn1lem11  36061  cbvoprab3davw  36239  bj-dfid2ALT  37031  bj-endval  37281  csbfinxpg  37354  finixpnum  37565  ldualset  39081  tgrpfset  40701  tgrpset  40702  erngfset  40756  erngset  40757  erngfset-rN  40764  erngset-rN  40765  dvafset  40961  dvaset  40962  dvhfset  41037  dvhset  41038  dvhfvadd  41048  dvhopvadd2  41051  dib1dim2  41125  dicvscacl  41148  cdlemn6  41159  dihopelvalcpre  41205  dih1dimatlem  41286  hdmapfval  41784  hlhilset  41891  mendval  43140  mnringvald  44177  ovolval4lem1  46570  ovolval4lem2  46571  ovnovollem3  46579  isubgrvtxuhgr  47736  isubgr0uhgr  47743  rngcvalALTV  47988  ringcvalALTV  48012  zlmodzxzsub  48085  lmod1zr  48222  2arymaptf  48386  prstcval  48731  mndtcval  48752