Theorem opeq2d 4846

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

Syntax hints:   → wi 4   = wceq 1567  ⟨cop 4597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is referenced by:  dfid2  5556  funopsn  7142  funopsnOLD  7143  fmptsng  7164  fmptsnd  7165  fvproj  8126  tfrlem11  8371  seqomlem0  8432  seqomlem1  8433  seqomlem4  8436  seqomeq12  8437  fundmen  9024  dif1en  9142  unxpdomlem1  9212  mulcanenq  10941  elreal2  11113  om2uzrdg  13988  uzrdgsuci  13992  seqeq2  14037  seqeq3  14038  s1val  14632  s1eq  14634  swrdlsw  14701  pfxpfx  14741  swrdccat  14768  swrdccat3blem  14772  swrdccat3b  14773  pfxccatin12d  14778  swrds2  14973  swrds2m  14974  swrd2lsw  14985  eucalgval  16636  setsidvald  17255  ressval  17289  ressress  17303  prdsval  17504  imasval  17561  imasaddvallem  17579  xpsfval  17616  xpsval  17620  cidval  17729  iscatd2  17733  oppcval  17765  ismon  17786  rescval  17880  idfucl  17934  funcres  17949  idfusubc0  17952  idfusubc  17953  fucval  18014  fucpropd  18033  setcval  18130  catcval  18153  estrcval  18176  xpcval  18229  1stfcl  18249  2ndfcl  18250  curf12  18279  curf2val  18282  curfcl  18284  hofcl  18311  oduval  18340  ipoval  18582  frmdval  18906  efmnd  18925  oppgval  19413  symgvalstruct  19463  efgmval  19778  efgmnvl  19780  efgi  19785  frgpup3lem  19843  dprd2da  20110  dmdprdpr  20117  dprdpr  20118  pgpfaclem1  20149  mgpval  20215  mgpress  20222  opprval  20416  sraval  21270  rlmval2  21287  pzriprnglem10  21605  zlmval  21630  znval  21650  znval2  21652  thlval  21810  islindf4  21953  psrval  22030  opsrval  22162  opsrval2  22164  matval  22533  mat1dimmul  22598  mat1dimcrng  22599  mat1scmat  22661  mdet0pr  22714  m1detdiag  22719  txkgen  23774  pt1hmeo  23928  xpstopnlem1  23931  xpstopnlem2  23933  tusval  24387  tmsval  24603  tngval  24761  om1val  25154  pi1xfrcnvlem  25180  pi1xfrcnv  25181  dchrval  27360  nosupbnd2lem1  27841  noinfbnd2lem1  27856  seqseq123d  28441  om2noseqrdg  28459  noseqrdgsuc  28463  ttgval  29161  eengv  29266  uspgr1ewop  29535  usgr2v1e2w  29539  1loopgruspgr  29787  1egrvtxdg1r  29797  1egrvtxdg0  29798  eupth2lem3lem3  30518  eupth2  30527  wlkl0  30655  br8d  32890  fresunsn  32907  elrgspnlem2  33500  rlocval  33516  rlocf1  33531  resvval  33588  opprabs  33705  idlsrgval  33734  selvply1rhmlema  33849  selvply1rhmlemb  33850  selvply1rhmlem1  33851  selvply1rhmlem3  33853  selvply1rhmlem5  33855  selvply1rhm  33856  mplidom  33859  extvfvcl  33867  resssra  33918  smatfval  34126  smatrcl  34127  smatlem  34128  qqhval  34303  bnj66  35189  bnj1234  35342  bnj1296  35350  bnj1450  35379  bnj1463  35384  bnj1501  35396  bnj1523  35400  subfacp1lem5  35571  cvmliftlem10  35681  cvmlift2lem12  35701  goaleq12d  35738  sategoelfvb  35806  msubffval  35910  msubfval  35911  elmsubrn  35915  msubrn  35916  msubco  35918  br8  36143  br6  36144  btwnouttr2  36409  brfs  36466  btwnconn1lem11  36484  cbvoprab3davw  36670  bj-dfid2ALT  37585  bj-endval  37842  csbfinxpg  37917  finixpnum  38139  ldualset  39784  tgrpfset  41403  tgrpset  41404  erngfset  41458  erngset  41459  erngfset-rN  41466  erngset-rN  41467  dvafset  41663  dvaset  41664  dvhfset  41739  dvhset  41740  dvhfvadd  41750  dvhopvadd2  41753  dib1dim2  41827  dicvscacl  41850  cdlemn6  41861  dihopelvalcpre  41907  dih1dimatlem  41988  hdmapfval  42486  hlhilset  42593  mendval  43791  mnringvald  44822  ovolval4lem1  47248  ovolval4lem2  47249  ovnovollem3  47257  isubgrvtxuhgr  48511  isubgr0uhgr  48520  stgrfv  48600  gpgov  48689  gpgprismgriedgdmss  48699  gpgvtx0  48700  gpgvtx1  48701  gpgedgvtx0  48708  gpgedgvtx1  48709  gpgvtxedg0  48710  gpgvtxedg1  48711  gpgedgiov  48712  gpgedg2ov  48713  gpgedg2iv  48714  gpg3kgrtriexlem6  48735  gpg3kgrtriex  48736  gpgprismgr4cycllem3  48744  pgnbgreunbgrlem1  48760  pgnbgreunbgrlem2  48764  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5  48770  gpg5edgnedg  48777  rngcvalALTV  48912  ringcvalALTV  48936  zlmodzxzsub  49018  lmod1zr  49151  2arymaptf  49310  discsubc  49720  2oppf  49788  upfval2  49833  upfval3  49834  isuplem  49835  uptpos  49854  uptr2  49877  dfswapf2  49917  oppc1stf  49944  oppc2ndf  49945  fucolid  50017  fucorid  50018  precofval2  50025  prcofval  50034  isinito2lem  50154  termcfuncval  50188  prstcval  50207  mndtcval  50235  lanup  50297  coccom  50320  iscmd  50322