Theorem opeq2d 4834

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  dfid2  5520  funopsn  7086  fmptsng  7108  fmptsnd  7109  fvproj  8074  tfrlem11  8317  seqomlem0  8378  seqomlem1  8379  seqomlem4  8382  seqomeq12  8383  fundmen  8963  dif1en  9084  dif1enOLD  9086  unxpdomlem1  9155  mulcanenq  10873  elreal2  11045  om2uzrdg  13881  uzrdgsuci  13885  seqeq2  13930  seqeq3  13931  s1val  14523  s1eq  14525  swrdlsw  14592  pfxpfx  14632  swrdccat  14659  swrdccat3blem  14663  swrdccat3b  14664  pfxccatin12d  14669  swrds2  14865  swrds2m  14866  swrd2lsw  14877  eucalgval  16511  setsidvald  17128  ressval  17162  ressress  17176  prdsval  17377  imasval  17433  imasaddvallem  17451  xpsfval  17488  xpsval  17492  cidval  17601  iscatd2  17605  oppcval  17637  ismon  17658  rescval  17752  idfucl  17806  funcres  17821  idfusubc0  17824  idfusubc  17825  fucval  17886  fucpropd  17905  setcval  18002  catcval  18025  estrcval  18048  xpcval  18101  1stfcl  18121  2ndfcl  18122  curf12  18151  curf2val  18154  curfcl  18156  hofcl  18183  oduval  18212  ipoval  18454  frmdval  18743  efmnd  18762  oppgval  19244  symgvalstruct  19294  efgmval  19609  efgmnvl  19611  efgi  19616  frgpup3lem  19674  dprd2da  19941  dmdprdpr  19948  dprdpr  19949  pgpfaclem1  19980  mgpval  20046  mgpress  20053  opprval  20241  sraval  21097  rlmval2  21114  pzriprnglem10  21415  zlmval  21440  znval  21460  znval2  21462  thlval  21620  islindf4  21763  psrval  21840  opsrval  21969  opsrval2  21971  matval  22314  mat1dimmul  22379  mat1dimcrng  22380  mat1scmat  22442  mdet0pr  22495  m1detdiag  22500  txkgen  23555  pt1hmeo  23709  xpstopnlem1  23712  xpstopnlem2  23714  tusval  24169  tmsval  24385  tngval  24543  om1val  24946  pi1xfrcnvlem  24972  pi1xfrcnv  24973  dchrval  27161  nosupbnd2lem1  27643  noinfbnd2lem1  27658  seqseq123d  28203  om2noseqrdg  28221  noseqrdgsuc  28225  ttgval  28838  eengv  28942  uspgr1ewop  29211  usgr2v1e2w  29215  1loopgruspgr  29464  1egrvtxdg1r  29474  1egrvtxdg0  29475  eupth2lem3lem3  30192  eupth2  30201  wlkl0  30329  br8d  32571  elrgspnlem2  33196  rlocval  33212  rlocf1  33226  resvval  33280  opprabs  33432  idlsrgval  33453  resssra  33562  smatfval  33764  smatrcl  33765  smatlem  33766  qqhval  33941  bnj66  34829  bnj1234  34982  bnj1296  34990  bnj1450  35019  bnj1463  35024  bnj1501  35036  bnj1523  35040  subfacp1lem5  35159  cvmliftlem10  35269  cvmlift2lem12  35289  goaleq12d  35326  sategoelfvb  35394  msubffval  35498  msubfval  35499  elmsubrn  35503  msubrn  35504  msubco  35506  br8  35731  br6  35732  btwnouttr2  35998  brfs  36055  btwnconn1lem11  36073  cbvoprab3davw  36249  bj-dfid2ALT  37041  bj-endval  37291  csbfinxpg  37364  finixpnum  37587  ldualset  39106  tgrpfset  40726  tgrpset  40727  erngfset  40781  erngset  40782  erngfset-rN  40789  erngset-rN  40790  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  dvhfvadd  41073  dvhopvadd2  41076  dib1dim2  41150  dicvscacl  41173  cdlemn6  41184  dihopelvalcpre  41230  dih1dimatlem  41311  hdmapfval  41809  hlhilset  41916  mendval  43155  mnringvald  44189  ovolval4lem1  46634  ovolval4lem2  46635  ovnovollem3  46643  isubgrvtxuhgr  47852  isubgr0uhgr  47861  stgrfv  47941  gpgov  48030  gpgprismgriedgdmss  48040  gpgvtx0  48041  gpgvtx1  48042  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  gpg3kgrtriexlem6  48076  gpg3kgrtriex  48077  gpgprismgr4cycllem3  48085  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  gpg5edgnedg  48118  rngcvalALTV  48253  ringcvalALTV  48277  zlmodzxzsub  48348  lmod1zr  48482  2arymaptf  48641  discsubc  49053  2oppf  49121  upfval2  49166  upfval3  49167  isuplem  49168  uptpos  49187  uptr2  49210  dfswapf2  49250  oppc1stf  49277  oppc2ndf  49278  fucolid  49350  fucorid  49351  precofval2  49358  prcofval  49367  isinito2lem  49487  termcfuncval  49521  prstcval  49540  mndtcval  49568  lanup  49630  coccom  49653  iscmd  49655