Theorem opeq2d 4847

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4597

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598

This theorem is used by:  dfid2  5560  funopsn  7148  funopsnOLD  7149  fmptsng  7170  fmptsnd  7171  fvproj  8132  tfrlem11  8377  seqomlem0  8438  seqomlem1  8439  seqomlem4  8442  seqomeq12  8443  fundmen  9031  dif1en  9149  unxpdomlem1  9219  mulcanenq  10956  elreal2  11128  om2uzrdg  14005  uzrdgsuci  14009  seqeq2  14054  seqeq3  14055  s1val  14650  s1eq  14652  swrdlsw  14722  pfxpfx  14762  swrdccat  14789  swrdccat3blem  14793  swrdccat3b  14794  pfxccatin12d  14799  swrds2  14996  swrds2m  14997  swrd2lsw  15008  eucalgval  16657  setsidvald  17276  ressval  17310  ressress  17324  prdsval  17525  imasval  17582  imasaddvallem  17600  xpsfval  17637  xpsval  17641  cidval  17750  iscatd2  17754  oppcval  17786  ismon  17807  rescval  17901  idfucl  17955  funcres  17970  idfusubc0  17973  idfusubc  17974  fucval  18035  fucpropd  18054  setcval  18151  catcval  18174  estrcval  18197  xpcval  18250  1stfcl  18270  2ndfcl  18271  curf12  18300  curf2val  18303  curfcl  18305  hofcl  18332  oduval  18361  ipoval  18603  frmdval  18933  efmnd  18952  oppgval  19440  symgvalstruct  19490  efgmval  19805  efgmnvl  19807  efgi  19812  frgpup3lem  19870  dprd2da  20137  dmdprdpr  20144  dprdpr  20145  pgpfaclem1  20176  mgpval  20242  mgpress  20249  opprval  20445  sraval  21325  rlmval2  21342  pzriprnglem10  21669  zlmval  21694  znval  21714  znval2  21716  thlval  21874  islindf4  22017  psrval  22094  opsrval  22226  opsrval2  22228  matval  22597  mat1dimmul  22662  mat1dimcrng  22663  mat1scmat  22725  mdet0pr  22778  m1detdiag  22783  txkgen  23838  pt1hmeo  23992  xpstopnlem1  23995  xpstopnlem2  23997  tusval  24451  tmsval  24667  tngval  24825  om1val  25218  pi1xfrcnvlem  25244  pi1xfrcnv  25245  dchrval  27427  nosupbnd2lem1  27908  noinfbnd2lem1  27923  seqseq123d  28508  om2noseqrdg  28526  noseqrdgsuc  28530  ttgval  29253  eengv  29358  uspgr1ewop  29627  usgr2v1e2w  29631  1loopgruspgr  29879  1egrvtxdg1r  29889  1egrvtxdg0  29890  eupth2lem3lem3  30610  eupth2  30619  wlkl0  30747  br8d  32982  fresunsn  32999  elrgspnlem2  33586  rlocval  33602  rlocf1  33617  resvval  33672  opprabs  33787  idlsrgval  33816  selvply1rhmlema  33931  selvply1rhmlemb  33932  selvply1rhmlem1  33933  selvply1rhmlem3  33935  selvply1rhmlem5  33937  selvply1rhm  33938  mplidom  33941  extvfvcl  33949  resssra  34000  smatfval  34208  smatrcl  34209  smatlem  34210  qqhval  34385  bnj66  35272  bnj1234  35425  bnj1296  35433  bnj1450  35462  bnj1463  35467  bnj1501  35479  bnj1523  35483  subfacp1lem5  35689  cvmliftlem10  35799  cvmlift2lem12  35819  goaleq12d  35856  sategoelfvb  35924  msubffval  36028  msubfval  36029  elmsubrn  36033  msubrn  36034  msubco  36036  br8  36261  br6  36262  btwnouttr2  36527  brfs  36584  btwnconn1lem11  36602  cbvoprab3davw  36818  bj-dfid2ALT  37734  bj-endval  37992  csbfinxpg  38067  finixpnum  38289  ldualset  39932  tgrpfset  41551  tgrpset  41552  erngfset  41606  erngset  41607  erngfset-rN  41614  erngset-rN  41615  dvafset  41811  dvaset  41812  dvhfset  41887  dvhset  41888  dvhfvadd  41898  dvhopvadd2  41901  dib1dim2  41975  dicvscacl  41998  cdlemn6  42009  dihopelvalcpre  42055  dih1dimatlem  42136  hdmapfval  42634  hlhilset  42741  mendval  43939  mnringvald  44970  ovolval4lem1  47396  ovolval4lem2  47397  ovnovollem3  47405  isubgrvtxuhgr  48662  isubgr0uhgr  48671  stgrfv  48751  gpgov  48840  gpgprismgriedgdmss  48850  gpgvtx0  48851  gpgvtx1  48852  gpgedgvtx0  48859  gpgedgvtx1  48860  gpgvtxedg0  48861  gpgvtxedg1  48862  gpgedgiov  48863  gpgedg2ov  48864  gpgedg2iv  48865  gpg3kgrtriexlem6  48886  gpg3kgrtriex  48887  gpgprismgr4cycllem3  48895  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5  48921  gpg5edgnedg  48928  rngcvalALTV  49063  ringcvalALTV  49087  zlmodzxzsub  49173  lmod1zr  49306  2arymaptf  49465  discsubc  49875  2oppf  49943  upfval2  49988  upfval3  49989  isuplem  49990  uptpos  50009  uptr2  50032  dfswapf2  50072  oppc1stf  50099  oppc2ndf  50100  fucolid  50172  fucorid  50173  precofval2  50180  prcofval  50189  isinito2lem  50309  termcfuncval  50343  prstcval  50362  mndtcval  50390  lanup  50452  coccom  50475  iscmd  50477