Theorem opeq2d 4777

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

Syntax hints:   → wi 4   = wceq 1543  ⟨cop 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534

This theorem is referenced by:  funopsn  6941  fmptsng  6961  fmptsnd  6962  fvproj  7879  tfrlem11  8102  seqomlem0  8163  seqomlem1  8164  seqomlem4  8167  seqomeq12  8168  fundmen  8686  dif1en  8818  unxpdomlem1  8858  mulcanenq  10539  elreal2  10711  om2uzrdg  13494  uzrdgsuci  13498  seqeq2  13543  seqeq3  13544  s1val  14120  s1eq  14122  swrdlsw  14197  pfxpfx  14238  swrdccat  14265  swrdccat3blem  14269  swrdccat3b  14270  pfxccatin12d  14275  swrds2  14470  swrds2m  14471  swrd2lsw  14482  eucalgval  16102  setsidvald  16696  ressval  16735  ressress  16746  prdsval  16914  imasval  16970  imasaddvallem  16988  xpsfval  17025  xpsval  17029  cidval  17134  iscatd2  17138  oppcval  17170  ismon  17192  rescval  17286  idfucl  17341  funcres  17356  fucval  17420  fucpropd  17440  setcval  17537  catcval  17560  estrcval  17585  xpcval  17638  1stfcl  17658  2ndfcl  17659  curf12  17689  curf2val  17692  curfcl  17694  hofcl  17721  oduval  17750  ipoval  17990  frmdval  18232  efmnd  18251  oppgval  18693  symgvalstruct  18743  efgmval  19056  efgmnvl  19058  efgi  19063  frgpup3lem  19121  dprd2da  19383  dmdprdpr  19390  dprdpr  19391  pgpfaclem1  19422  mgpval  19461  mgpress  19469  opprval  19596  sraval  20167  rlmval2  20185  zlmval  20436  znval  20454  znval2  20456  thlval  20611  islindf4  20754  psrval  20828  opsrval  20957  opsrval2  20959  matval  21262  mat1dimmul  21327  mat1dimcrng  21328  mat1scmat  21390  mdet0pr  21443  m1detdiag  21448  txkgen  22503  pt1hmeo  22657  xpstopnlem1  22660  xpstopnlem2  22662  tusval  23117  tmsval  23333  tngval  23491  om1val  23881  pi1xfrcnvlem  23907  pi1xfrcnv  23908  dchrval  26069  ttgval  26920  eengv  27024  uspgr1ewop  27290  usgr2v1e2w  27294  1loopgruspgr  27542  1egrvtxdg1r  27552  1egrvtxdg0  27553  eupth2lem3lem3  28267  eupth2  28276  wlkl0  28404  br8d  30623  resvval  31199  idlsrgval  31316  smatfval  31413  smatrcl  31414  smatlem  31415  qqhval  31590  bnj66  32507  bnj1234  32660  bnj1296  32668  bnj1450  32697  bnj1463  32702  bnj1501  32714  bnj1523  32718  subfacp1lem5  32813  cvmliftlem10  32923  cvmlift2lem12  32943  goaleq12d  32980  sategoelfvb  33048  msubffval  33152  msubfval  33153  elmsubrn  33157  msubrn  33158  msubco  33160  br8  33393  br6  33394  nosupbnd2lem1  33604  noinfbnd2lem1  33619  btwnouttr2  34010  brfs  34067  btwnconn1lem11  34085  bj-endval  35169  csbfinxpg  35245  finixpnum  35448  ldualset  36825  tgrpfset  38444  tgrpset  38445  erngfset  38499  erngset  38500  erngfset-rN  38507  erngset-rN  38508  dvafset  38704  dvaset  38705  dvhfset  38780  dvhset  38781  dvhfvadd  38791  dvhopvadd2  38794  dib1dim2  38868  dicvscacl  38891  cdlemn6  38902  dihopelvalcpre  38948  dih1dimatlem  39029  hdmapfval  39527  hlhilset  39634  mendval  40652  mnringvald  41445  ovolval4lem1  43805  ovolval4lem2  43806  ovnovollem3  43814  idfusubc0  45039  idfusubc  45040  rngcvalALTV  45135  ringcvalALTV  45181  zlmodzxzsub  45312  lmod1zr  45450  2arymaptf  45614  prstcval  45961  mndtcval  45980