Theorem opeq2d 4824

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4574

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  dfid2  5521  funopsn  7095  fmptsng  7116  fmptsnd  7117  fvproj  8077  tfrlem11  8320  seqomlem0  8381  seqomlem1  8382  seqomlem4  8385  seqomeq12  8386  fundmen  8971  dif1en  9089  unxpdomlem1  9159  mulcanenq  10874  elreal2  11046  om2uzrdg  13909  uzrdgsuci  13913  seqeq2  13958  seqeq3  13959  s1val  14552  s1eq  14554  swrdlsw  14621  pfxpfx  14661  swrdccat  14688  swrdccat3blem  14692  swrdccat3b  14693  pfxccatin12d  14698  swrds2  14893  swrds2m  14894  swrd2lsw  14905  eucalgval  16542  setsidvald  17160  ressval  17194  ressress  17208  prdsval  17409  imasval  17466  imasaddvallem  17484  xpsfval  17521  xpsval  17525  cidval  17634  iscatd2  17638  oppcval  17670  ismon  17691  rescval  17785  idfucl  17839  funcres  17854  idfusubc0  17857  idfusubc  17858  fucval  17919  fucpropd  17938  setcval  18035  catcval  18058  estrcval  18081  xpcval  18134  1stfcl  18154  2ndfcl  18155  curf12  18184  curf2val  18187  curfcl  18189  hofcl  18216  oduval  18245  ipoval  18487  frmdval  18810  efmnd  18829  oppgval  19313  symgvalstruct  19363  efgmval  19678  efgmnvl  19680  efgi  19685  frgpup3lem  19743  dprd2da  20010  dmdprdpr  20017  dprdpr  20018  pgpfaclem1  20049  mgpval  20115  mgpress  20122  opprval  20309  sraval  21162  rlmval2  21179  pzriprnglem10  21480  zlmval  21505  znval  21525  znval2  21527  thlval  21685  islindf4  21828  psrval  21905  opsrval  22034  opsrval2  22036  matval  22386  mat1dimmul  22451  mat1dimcrng  22452  mat1scmat  22514  mdet0pr  22567  m1detdiag  22572  txkgen  23627  pt1hmeo  23781  xpstopnlem1  23784  xpstopnlem2  23786  tusval  24240  tmsval  24456  tngval  24614  om1val  25007  pi1xfrcnvlem  25033  pi1xfrcnv  25034  dchrval  27211  nosupbnd2lem1  27693  noinfbnd2lem1  27708  seqseq123d  28292  om2noseqrdg  28310  noseqrdgsuc  28314  ttgval  28957  eengv  29062  uspgr1ewop  29331  usgr2v1e2w  29335  1loopgruspgr  29584  1egrvtxdg1r  29594  1egrvtxdg0  29595  eupth2lem3lem3  30315  eupth2  30324  wlkl0  30452  br8d  32696  fresunsn  32713  elrgspnlem2  33319  rlocval  33335  rlocf1  33349  resvval  33404  opprabs  33557  idlsrgval  33578  extvfvcl  33695  resssra  33746  smatfval  33955  smatrcl  33956  smatlem  33957  qqhval  34132  bnj66  35018  bnj1234  35171  bnj1296  35179  bnj1450  35208  bnj1463  35213  bnj1501  35225  bnj1523  35229  subfacp1lem5  35382  cvmliftlem10  35492  cvmlift2lem12  35512  goaleq12d  35549  sategoelfvb  35617  msubffval  35721  msubfval  35722  elmsubrn  35726  msubrn  35727  msubco  35729  br8  35954  br6  35955  btwnouttr2  36220  brfs  36277  btwnconn1lem11  36295  cbvoprab3davw  36471  bj-dfid2ALT  37388  bj-endval  37645  csbfinxpg  37718  finixpnum  37940  ldualset  39585  tgrpfset  41204  tgrpset  41205  erngfset  41259  erngset  41260  erngfset-rN  41267  erngset-rN  41268  dvafset  41464  dvaset  41465  dvhfset  41540  dvhset  41541  dvhfvadd  41551  dvhopvadd2  41554  dib1dim2  41628  dicvscacl  41651  cdlemn6  41662  dihopelvalcpre  41708  dih1dimatlem  41789  hdmapfval  42287  hlhilset  42394  mendval  43625  mnringvald  44658  ovolval4lem1  47095  ovolval4lem2  47096  ovnovollem3  47104  isubgrvtxuhgr  48352  isubgr0uhgr  48361  stgrfv  48441  gpgov  48530  gpgprismgriedgdmss  48540  gpgvtx0  48541  gpgvtx1  48542  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgvtxedg0  48551  gpgvtxedg1  48552  gpgedgiov  48553  gpgedg2ov  48554  gpgedg2iv  48555  gpg3kgrtriexlem6  48576  gpg3kgrtriex  48577  gpgprismgr4cycllem3  48585  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2  48605  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5  48611  gpg5edgnedg  48618  rngcvalALTV  48753  ringcvalALTV  48777  zlmodzxzsub  48848  lmod1zr  48981  2arymaptf  49140  discsubc  49551  2oppf  49619  upfval2  49664  upfval3  49665  isuplem  49666  uptpos  49685  uptr2  49708  dfswapf2  49748  oppc1stf  49775  oppc2ndf  49776  fucolid  49848  fucorid  49849  precofval2  49856  prcofval  49865  isinito2lem  49985  termcfuncval  50019  prstcval  50038  mndtcval  50066  lanup  50128  coccom  50151  iscmd  50153