Theorem opeq2d 4880

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635

This theorem is referenced by:  dfid2  5576  funopsn  7148  fmptsng  7168  fmptsnd  7169  fvproj  8122  tfrlem11  8390  seqomlem0  8451  seqomlem1  8452  seqomlem4  8455  seqomeq12  8456  fundmen  9033  dif1en  9162  dif1enOLD  9164  unxpdomlem1  9252  mulcanenq  10957  elreal2  11129  om2uzrdg  13925  uzrdgsuci  13929  seqeq2  13974  seqeq3  13975  s1val  14552  s1eq  14554  swrdlsw  14621  pfxpfx  14662  swrdccat  14689  swrdccat3blem  14693  swrdccat3b  14694  pfxccatin12d  14699  swrds2  14895  swrds2m  14896  swrd2lsw  14907  eucalgval  16523  setsidvald  17136  setsidvaldOLD  17137  ressval  17180  ressress  17197  prdsval  17405  imasval  17461  imasaddvallem  17479  xpsfval  17516  xpsval  17520  cidval  17625  iscatd2  17629  oppcval  17661  ismon  17684  rescval  17778  idfucl  17835  funcres  17850  fucval  17914  fucpropd  17934  setcval  18031  catcval  18054  estrcval  18079  xpcval  18133  1stfcl  18153  2ndfcl  18154  curf12  18184  curf2val  18187  curfcl  18189  hofcl  18216  oduval  18245  ipoval  18487  frmdval  18768  efmnd  18787  oppgval  19252  symgvalstruct  19305  symgvalstructOLD  19306  efgmval  19621  efgmnvl  19623  efgi  19628  frgpup3lem  19686  dprd2da  19953  dmdprdpr  19960  dprdpr  19961  pgpfaclem1  19992  mgpval  20031  mgpress  20043  mgpressOLD  20044  opprval  20226  sraval  20934  rlmval2  20961  pzriprnglem10  21259  zlmval  21284  znval  21306  znval2  21308  thlval  21467  islindf4  21612  psrval  21687  opsrval  21820  opsrval2  21822  matval  22131  mat1dimmul  22198  mat1dimcrng  22199  mat1scmat  22261  mdet0pr  22314  m1detdiag  22319  txkgen  23376  pt1hmeo  23530  xpstopnlem1  23533  xpstopnlem2  23535  tusval  23990  tmsval  24209  tngval  24368  om1val  24770  pi1xfrcnvlem  24796  pi1xfrcnv  24797  dchrval  26961  nosupbnd2lem1  27442  noinfbnd2lem1  27457  ttgval  28381  ttgvalOLD  28382  eengv  28492  uspgr1ewop  28760  usgr2v1e2w  28764  1loopgruspgr  29012  1egrvtxdg1r  29022  1egrvtxdg0  29023  eupth2lem3lem3  29738  eupth2  29747  wlkl0  29875  br8d  32094  resvval  32699  opprabs  32858  idlsrgval  32879  resssra  32950  smatfval  33061  smatrcl  33062  smatlem  33063  qqhval  33240  bnj66  34157  bnj1234  34310  bnj1296  34318  bnj1450  34347  bnj1463  34352  bnj1501  34364  bnj1523  34368  subfacp1lem5  34461  cvmliftlem10  34571  cvmlift2lem12  34591  goaleq12d  34628  sategoelfvb  34696  msubffval  34800  msubfval  34801  elmsubrn  34805  msubrn  34806  msubco  34808  br8  35018  br6  35019  btwnouttr2  35286  brfs  35343  btwnconn1lem11  35361  bj-dfid2ALT  36249  bj-endval  36499  csbfinxpg  36572  finixpnum  36776  ldualset  38298  tgrpfset  39918  tgrpset  39919  erngfset  39973  erngset  39974  erngfset-rN  39981  erngset-rN  39982  dvafset  40178  dvaset  40179  dvhfset  40254  dvhset  40255  dvhfvadd  40265  dvhopvadd2  40268  dib1dim2  40342  dicvscacl  40365  cdlemn6  40376  dihopelvalcpre  40422  dih1dimatlem  40503  hdmapfval  41001  hlhilset  41108  mendval  42227  mnringvald  43269  ovolval4lem1  45664  ovolval4lem2  45665  ovnovollem3  45673  idfusubc0  46906  idfusubc  46907  rngcvalALTV  46948  ringcvalALTV  46994  zlmodzxzsub  47125  lmod1zr  47262  2arymaptf  47426  prstcval  47772  mndtcval  47793