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 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  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  8964  dif1en  9082  unxpdomlem1  9151  mulcanenq  10862  elreal2  11034  om2uzrdg  13870  uzrdgsuci  13874  seqeq2  13919  seqeq3  13920  s1val  14513  s1eq  14515  swrdlsw  14582  pfxpfx  14622  swrdccat  14649  swrdccat3blem  14653  swrdccat3b  14654  pfxccatin12d  14659  swrds2  14854  swrds2m  14855  swrd2lsw  14866  eucalgval  16500  setsidvald  17117  ressval  17151  ressress  17165  prdsval  17366  imasval  17423  imasaddvallem  17441  xpsfval  17478  xpsval  17482  cidval  17591  iscatd2  17595  oppcval  17627  ismon  17648  rescval  17742  idfucl  17796  funcres  17811  idfusubc0  17814  idfusubc  17815  fucval  17876  fucpropd  17895  setcval  17992  catcval  18015  estrcval  18038  xpcval  18091  1stfcl  18111  2ndfcl  18112  curf12  18141  curf2val  18144  curfcl  18146  hofcl  18173  oduval  18202  ipoval  18444  frmdval  18767  efmnd  18786  oppgval  19267  symgvalstruct  19317  efgmval  19632  efgmnvl  19634  efgi  19639  frgpup3lem  19697  dprd2da  19964  dmdprdpr  19971  dprdpr  19972  pgpfaclem1  20003  mgpval  20069  mgpress  20076  opprval  20265  sraval  21118  rlmval2  21135  pzriprnglem10  21436  zlmval  21461  znval  21481  znval2  21483  thlval  21641  islindf4  21784  psrval  21862  opsrval  21992  opsrval2  21994  matval  22346  mat1dimmul  22411  mat1dimcrng  22412  mat1scmat  22474  mdet0pr  22527  m1detdiag  22532  txkgen  23587  pt1hmeo  23741  xpstopnlem1  23744  xpstopnlem2  23746  tusval  24200  tmsval  24416  tngval  24574  om1val  24977  pi1xfrcnvlem  25003  pi1xfrcnv  25004  dchrval  27192  nosupbnd2lem1  27674  noinfbnd2lem1  27689  seqseq123d  28236  om2noseqrdg  28254  noseqrdgsuc  28258  ttgval  28873  eengv  28978  uspgr1ewop  29247  usgr2v1e2w  29251  1loopgruspgr  29500  1egrvtxdg1r  29510  1egrvtxdg0  29511  eupth2lem3lem3  30231  eupth2  30240  wlkl0  30368  br8d  32612  fresunsn  32629  elrgspnlem2  33253  rlocval  33269  rlocf1  33283  resvval  33338  opprabs  33491  idlsrgval  33512  extvfvcl  33629  resssra  33671  smatfval  33880  smatrcl  33881  smatlem  33882  qqhval  34057  bnj66  34944  bnj1234  35097  bnj1296  35105  bnj1450  35134  bnj1463  35139  bnj1501  35151  bnj1523  35155  subfacp1lem5  35300  cvmliftlem10  35410  cvmlift2lem12  35430  goaleq12d  35467  sategoelfvb  35535  msubffval  35639  msubfval  35640  elmsubrn  35644  msubrn  35645  msubco  35647  br8  35872  br6  35873  btwnouttr2  36138  brfs  36195  btwnconn1lem11  36213  cbvoprab3davw  36389  bj-dfid2ALT  37182  bj-endval  37432  csbfinxpg  37505  finixpnum  37718  ldualset  39297  tgrpfset  40916  tgrpset  40917  erngfset  40971  erngset  40972  erngfset-rN  40979  erngset-rN  40980  dvafset  41176  dvaset  41177  dvhfset  41252  dvhset  41253  dvhfvadd  41263  dvhopvadd2  41266  dib1dim2  41340  dicvscacl  41363  cdlemn6  41374  dihopelvalcpre  41420  dih1dimatlem  41501  hdmapfval  41999  hlhilset  42106  mendval  43336  mnringvald  44370  ovolval4lem1  46809  ovolval4lem2  46810  ovnovollem3  46818  isubgrvtxuhgr  48026  isubgr0uhgr  48035  stgrfv  48115  gpgov  48204  gpgprismgriedgdmss  48214  gpgvtx0  48215  gpgvtx1  48216  gpgedgvtx0  48223  gpgedgvtx1  48224  gpgvtxedg0  48225  gpgvtxedg1  48226  gpgedgiov  48227  gpgedg2ov  48228  gpgedg2iv  48229  gpg3kgrtriexlem6  48250  gpg3kgrtriex  48251  gpgprismgr4cycllem3  48259  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5  48285  gpg5edgnedg  48292  rngcvalALTV  48427  ringcvalALTV  48451  zlmodzxzsub  48522  lmod1zr  48655  2arymaptf  48814  discsubc  49225  2oppf  49293  upfval2  49338  upfval3  49339  isuplem  49340  uptpos  49359  uptr2  49382  dfswapf2  49422  oppc1stf  49449  oppc2ndf  49450  fucolid  49522  fucorid  49523  precofval2  49530  prcofval  49539  isinito2lem  49659  termcfuncval  49693  prstcval  49712  mndtcval  49740  lanup  49802  coccom  49825  iscmd  49827