Theorem opeq2d 4832

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4582

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583

This theorem is referenced by:  dfid2  5513  funopsn  7081  fmptsng  7102  fmptsnd  7103  fvproj  8064  tfrlem11  8307  seqomlem0  8368  seqomlem1  8369  seqomlem4  8372  seqomeq12  8373  fundmen  8953  dif1en  9071  unxpdomlem1  9140  mulcanenq  10851  elreal2  11023  om2uzrdg  13863  uzrdgsuci  13867  seqeq2  13912  seqeq3  13913  s1val  14506  s1eq  14508  swrdlsw  14575  pfxpfx  14615  swrdccat  14642  swrdccat3blem  14646  swrdccat3b  14647  pfxccatin12d  14652  swrds2  14847  swrds2m  14848  swrd2lsw  14859  eucalgval  16493  setsidvald  17110  ressval  17144  ressress  17158  prdsval  17359  imasval  17415  imasaddvallem  17433  xpsfval  17470  xpsval  17474  cidval  17583  iscatd2  17587  oppcval  17619  ismon  17640  rescval  17734  idfucl  17788  funcres  17803  idfusubc0  17806  idfusubc  17807  fucval  17868  fucpropd  17887  setcval  17984  catcval  18007  estrcval  18030  xpcval  18083  1stfcl  18103  2ndfcl  18104  curf12  18133  curf2val  18136  curfcl  18138  hofcl  18165  oduval  18194  ipoval  18436  frmdval  18759  efmnd  18778  oppgval  19260  symgvalstruct  19310  efgmval  19625  efgmnvl  19627  efgi  19632  frgpup3lem  19690  dprd2da  19957  dmdprdpr  19964  dprdpr  19965  pgpfaclem1  19996  mgpval  20062  mgpress  20069  opprval  20257  sraval  21110  rlmval2  21127  pzriprnglem10  21428  zlmval  21453  znval  21473  znval2  21475  thlval  21633  islindf4  21776  psrval  21853  opsrval  21982  opsrval2  21984  matval  22327  mat1dimmul  22392  mat1dimcrng  22393  mat1scmat  22455  mdet0pr  22508  m1detdiag  22513  txkgen  23568  pt1hmeo  23722  xpstopnlem1  23725  xpstopnlem2  23727  tusval  24181  tmsval  24397  tngval  24555  om1val  24958  pi1xfrcnvlem  24984  pi1xfrcnv  24985  dchrval  27173  nosupbnd2lem1  27655  noinfbnd2lem1  27670  seqseq123d  28217  om2noseqrdg  28235  noseqrdgsuc  28239  ttgval  28854  eengv  28958  uspgr1ewop  29227  usgr2v1e2w  29231  1loopgruspgr  29480  1egrvtxdg1r  29490  1egrvtxdg0  29491  eupth2lem3lem3  30208  eupth2  30217  wlkl0  30345  br8d  32589  elrgspnlem2  33208  rlocval  33224  rlocf1  33238  resvval  33292  opprabs  33445  idlsrgval  33466  resssra  33597  smatfval  33806  smatrcl  33807  smatlem  33808  qqhval  33983  bnj66  34870  bnj1234  35023  bnj1296  35031  bnj1450  35060  bnj1463  35065  bnj1501  35077  bnj1523  35081  subfacp1lem5  35226  cvmliftlem10  35336  cvmlift2lem12  35356  goaleq12d  35393  sategoelfvb  35461  msubffval  35565  msubfval  35566  elmsubrn  35570  msubrn  35571  msubco  35573  br8  35798  br6  35799  btwnouttr2  36062  brfs  36119  btwnconn1lem11  36137  cbvoprab3davw  36313  bj-dfid2ALT  37105  bj-endval  37355  csbfinxpg  37428  finixpnum  37651  ldualset  39170  tgrpfset  40789  tgrpset  40790  erngfset  40844  erngset  40845  erngfset-rN  40852  erngset-rN  40853  dvafset  41049  dvaset  41050  dvhfset  41125  dvhset  41126  dvhfvadd  41136  dvhopvadd2  41139  dib1dim2  41213  dicvscacl  41236  cdlemn6  41247  dihopelvalcpre  41293  dih1dimatlem  41374  hdmapfval  41872  hlhilset  41979  mendval  43218  mnringvald  44252  ovolval4lem1  46693  ovolval4lem2  46694  ovnovollem3  46702  isubgrvtxuhgr  47901  isubgr0uhgr  47910  stgrfv  47990  gpgov  48079  gpgprismgriedgdmss  48089  gpgvtx0  48090  gpgvtx1  48091  gpgedgvtx0  48098  gpgedgvtx1  48099  gpgvtxedg0  48100  gpgvtxedg1  48101  gpgedgiov  48102  gpgedg2ov  48103  gpgedg2iv  48104  gpg3kgrtriexlem6  48125  gpg3kgrtriex  48126  gpgprismgr4cycllem3  48134  pgnbgreunbgrlem1  48150  pgnbgreunbgrlem2  48154  pgnbgreunbgrlem4  48156  pgnbgreunbgrlem5  48160  gpg5edgnedg  48167  rngcvalALTV  48302  ringcvalALTV  48326  zlmodzxzsub  48397  lmod1zr  48531  2arymaptf  48690  discsubc  49102  2oppf  49170  upfval2  49215  upfval3  49216  isuplem  49217  uptpos  49236  uptr2  49259  dfswapf2  49299  oppc1stf  49326  oppc2ndf  49327  fucolid  49399  fucorid  49400  precofval2  49407  prcofval  49416  isinito2lem  49536  termcfuncval  49570  prstcval  49589  mndtcval  49617  lanup  49679  coccom  49702  iscmd  49704