Theorem opeq2d 4833

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  dfid2  5518  funopsn  7090  fmptsng  7111  fmptsnd  7112  fvproj  8073  tfrlem11  8316  seqomlem0  8377  seqomlem1  8378  seqomlem4  8381  seqomeq12  8382  fundmen  8963  dif1en  9081  unxpdomlem1  9150  mulcanenq  10861  elreal2  11033  om2uzrdg  13873  uzrdgsuci  13877  seqeq2  13922  seqeq3  13923  s1val  14516  s1eq  14518  swrdlsw  14585  pfxpfx  14625  swrdccat  14652  swrdccat3blem  14656  swrdccat3b  14657  pfxccatin12d  14662  swrds2  14857  swrds2m  14858  swrd2lsw  14869  eucalgval  16503  setsidvald  17120  ressval  17154  ressress  17168  prdsval  17369  imasval  17425  imasaddvallem  17443  xpsfval  17480  xpsval  17484  cidval  17593  iscatd2  17597  oppcval  17629  ismon  17650  rescval  17744  idfucl  17798  funcres  17813  idfusubc0  17816  idfusubc  17817  fucval  17878  fucpropd  17897  setcval  17994  catcval  18017  estrcval  18040  xpcval  18093  1stfcl  18113  2ndfcl  18114  curf12  18143  curf2val  18146  curfcl  18148  hofcl  18175  oduval  18204  ipoval  18446  frmdval  18769  efmnd  18788  oppgval  19269  symgvalstruct  19319  efgmval  19634  efgmnvl  19636  efgi  19641  frgpup3lem  19699  dprd2da  19966  dmdprdpr  19973  dprdpr  19974  pgpfaclem1  20005  mgpval  20071  mgpress  20078  opprval  20266  sraval  21119  rlmval2  21136  pzriprnglem10  21437  zlmval  21462  znval  21482  znval2  21484  thlval  21642  islindf4  21785  psrval  21862  opsrval  21991  opsrval2  21993  matval  22336  mat1dimmul  22401  mat1dimcrng  22402  mat1scmat  22464  mdet0pr  22517  m1detdiag  22522  txkgen  23577  pt1hmeo  23731  xpstopnlem1  23734  xpstopnlem2  23736  tusval  24190  tmsval  24406  tngval  24564  om1val  24967  pi1xfrcnvlem  24993  pi1xfrcnv  24994  dchrval  27182  nosupbnd2lem1  27664  noinfbnd2lem1  27679  seqseq123d  28226  om2noseqrdg  28244  noseqrdgsuc  28248  ttgval  28863  eengv  28968  uspgr1ewop  29237  usgr2v1e2w  29241  1loopgruspgr  29490  1egrvtxdg1r  29500  1egrvtxdg0  29501  eupth2lem3lem3  30221  eupth2  30230  wlkl0  30358  br8d  32602  elrgspnlem2  33221  rlocval  33237  rlocf1  33251  resvval  33305  opprabs  33458  idlsrgval  33479  resssra  33610  smatfval  33819  smatrcl  33820  smatlem  33821  qqhval  33996  bnj66  34883  bnj1234  35036  bnj1296  35044  bnj1450  35073  bnj1463  35078  bnj1501  35090  bnj1523  35094  subfacp1lem5  35239  cvmliftlem10  35349  cvmlift2lem12  35369  goaleq12d  35406  sategoelfvb  35474  msubffval  35578  msubfval  35579  elmsubrn  35583  msubrn  35584  msubco  35586  br8  35811  br6  35812  btwnouttr2  36077  brfs  36134  btwnconn1lem11  36152  cbvoprab3davw  36328  bj-dfid2ALT  37120  bj-endval  37370  csbfinxpg  37443  finixpnum  37655  ldualset  39234  tgrpfset  40853  tgrpset  40854  erngfset  40908  erngset  40909  erngfset-rN  40916  erngset-rN  40917  dvafset  41113  dvaset  41114  dvhfset  41189  dvhset  41190  dvhfvadd  41200  dvhopvadd2  41203  dib1dim2  41277  dicvscacl  41300  cdlemn6  41311  dihopelvalcpre  41357  dih1dimatlem  41438  hdmapfval  41936  hlhilset  42043  mendval  43286  mnringvald  44320  ovolval4lem1  46761  ovolval4lem2  46762  ovnovollem3  46770  isubgrvtxuhgr  47978  isubgr0uhgr  47987  stgrfv  48067  gpgov  48156  gpgprismgriedgdmss  48166  gpgvtx0  48167  gpgvtx1  48168  gpgedgvtx0  48175  gpgedgvtx1  48176  gpgvtxedg0  48177  gpgvtxedg1  48178  gpgedgiov  48179  gpgedg2ov  48180  gpgedg2iv  48181  gpg3kgrtriexlem6  48202  gpg3kgrtriex  48203  gpgprismgr4cycllem3  48211  pgnbgreunbgrlem1  48227  pgnbgreunbgrlem2  48231  pgnbgreunbgrlem4  48233  pgnbgreunbgrlem5  48237  gpg5edgnedg  48244  rngcvalALTV  48379  ringcvalALTV  48403  zlmodzxzsub  48474  lmod1zr  48608  2arymaptf  48767  discsubc  49179  2oppf  49247  upfval2  49292  upfval3  49293  isuplem  49294  uptpos  49313  uptr2  49336  dfswapf2  49376  oppc1stf  49403  oppc2ndf  49404  fucolid  49476  fucorid  49477  precofval2  49484  prcofval  49493  isinito2lem  49613  termcfuncval  49647  prstcval  49666  mndtcval  49694  lanup  49756  coccom  49779  iscmd  49781