Theorem opeq2d 4818

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

Syntax hints:   → wi 4   = wceq 1547  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  dfid2  5522  funopsn  7097  funopsnOLD  7098  fmptsng  7119  fmptsnd  7120  fvproj  8081  tfrlem11  8324  seqomlem0  8385  seqomlem1  8386  seqomlem4  8389  seqomeq12  8390  fundmen  8975  dif1en  9093  unxpdomlem1  9163  mulcanenq  10881  elreal2  11053  om2uzrdg  13916  uzrdgsuci  13920  seqeq2  13965  seqeq3  13966  s1val  14559  s1eq  14561  swrdlsw  14628  pfxpfx  14668  swrdccat  14695  swrdccat3blem  14699  swrdccat3b  14700  pfxccatin12d  14705  swrds2  14900  swrds2m  14901  swrd2lsw  14912  eucalgval  16549  setsidvald  17167  ressval  17201  ressress  17215  prdsval  17416  imasval  17473  imasaddvallem  17491  xpsfval  17528  xpsval  17532  cidval  17641  iscatd2  17645  oppcval  17677  ismon  17698  rescval  17792  idfucl  17846  funcres  17861  idfusubc0  17864  idfusubc  17865  fucval  17926  fucpropd  17945  setcval  18042  catcval  18065  estrcval  18088  xpcval  18141  1stfcl  18161  2ndfcl  18162  curf12  18191  curf2val  18194  curfcl  18196  hofcl  18223  oduval  18252  ipoval  18494  frmdval  18817  efmnd  18836  oppgval  19320  symgvalstruct  19370  efgmval  19685  efgmnvl  19687  efgi  19692  frgpup3lem  19750  dprd2da  20017  dmdprdpr  20024  dprdpr  20025  pgpfaclem1  20056  mgpval  20122  mgpress  20129  opprval  20316  sraval  21172  rlmval2  21189  pzriprnglem10  21472  zlmval  21497  znval  21517  znval2  21519  thlval  21677  islindf4  21820  psrval  21897  opsrval  22029  opsrval2  22031  matval  22401  mat1dimmul  22466  mat1dimcrng  22467  mat1scmat  22529  mdet0pr  22582  m1detdiag  22587  txkgen  23642  pt1hmeo  23796  xpstopnlem1  23799  xpstopnlem2  23801  tusval  24255  tmsval  24471  tngval  24629  om1val  25022  pi1xfrcnvlem  25048  pi1xfrcnv  25049  dchrval  27222  nosupbnd2lem1  27704  noinfbnd2lem1  27719  seqseq123d  28303  om2noseqrdg  28321  noseqrdgsuc  28325  ttgval  28968  eengv  29073  uspgr1ewop  29342  usgr2v1e2w  29346  1loopgruspgr  29594  1egrvtxdg1r  29604  1egrvtxdg0  29605  eupth2lem3lem3  30325  eupth2  30334  wlkl0  30462  br8d  32707  fresunsn  32724  elrgspnlem2  33331  rlocval  33347  rlocf1  33361  resvval  33419  opprabs  33572  idlsrgval  33593  selvply1rhmlema  33709  selvply1rhmlemb  33710  selvply1rhmlem1  33711  selvply1rhmlem3  33713  selvply1rhmlem5  33715  selvply1rhm  33716  mplidom  33719  extvfvcl  33727  resssra  33778  smatfval  33986  smatrcl  33987  smatlem  33988  qqhval  34163  bnj66  35049  bnj1234  35202  bnj1296  35210  bnj1450  35239  bnj1463  35244  bnj1501  35256  bnj1523  35260  subfacp1lem5  35419  cvmliftlem10  35529  cvmlift2lem12  35549  goaleq12d  35586  sategoelfvb  35654  msubffval  35758  msubfval  35759  elmsubrn  35763  msubrn  35764  msubco  35766  br8  35991  br6  35992  btwnouttr2  36257  brfs  36314  btwnconn1lem11  36332  cbvoprab3davw  36508  bj-dfid2ALT  37425  bj-endval  37682  csbfinxpg  37757  finixpnum  37979  ldualset  39624  tgrpfset  41243  tgrpset  41244  erngfset  41298  erngset  41299  erngfset-rN  41306  erngset-rN  41307  dvafset  41503  dvaset  41504  dvhfset  41579  dvhset  41580  dvhfvadd  41590  dvhopvadd2  41593  dib1dim2  41667  dicvscacl  41690  cdlemn6  41701  dihopelvalcpre  41747  dih1dimatlem  41828  hdmapfval  42326  hlhilset  42433  mendval  43631  mnringvald  44664  ovolval4lem1  47099  ovolval4lem2  47100  ovnovollem3  47108  isubgrvtxuhgr  48362  isubgr0uhgr  48371  stgrfv  48451  gpgov  48540  gpgprismgriedgdmss  48550  gpgvtx0  48551  gpgvtx1  48552  gpgedgvtx0  48559  gpgedgvtx1  48560  gpgvtxedg0  48561  gpgvtxedg1  48562  gpgedgiov  48563  gpgedg2ov  48564  gpgedg2iv  48565  gpg3kgrtriexlem6  48586  gpg3kgrtriex  48587  gpgprismgr4cycllem3  48595  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2  48615  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5  48621  gpg5edgnedg  48628  rngcvalALTV  48763  ringcvalALTV  48787  zlmodzxzsub  48858  lmod1zr  48991  2arymaptf  49150  discsubc  49561  2oppf  49629  upfval2  49674  upfval3  49675  isuplem  49676  uptpos  49695  uptr2  49718  dfswapf2  49758  oppc1stf  49785  oppc2ndf  49786  fucolid  49858  fucorid  49859  precofval2  49866  prcofval  49875  isinito2lem  49995  termcfuncval  50029  prstcval  50048  mndtcval  50076  lanup  50138  coccom  50161  iscmd  50163