Theorem opeq2d 4846

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

Syntax hints:   → wi 4   = wceq 1570  ⟨cop 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597

This theorem is referenced by:  dfid2  5560  funopsn  7146  funopsnOLD  7147  fmptsng  7168  fmptsnd  7169  fvproj  8131  tfrlem11  8376  seqomlem0  8437  seqomlem1  8438  seqomlem4  8441  seqomeq12  8442  fundmen  9029  dif1en  9147  unxpdomlem1  9217  mulcanenq  10946  elreal2  11118  om2uzrdg  13994  uzrdgsuci  13998  seqeq2  14043  seqeq3  14044  s1val  14638  s1eq  14640  swrdlsw  14707  pfxpfx  14747  swrdccat  14774  swrdccat3blem  14778  swrdccat3b  14779  pfxccatin12d  14784  swrds2  14979  swrds2m  14980  swrd2lsw  14991  eucalgval  16641  setsidvald  17260  ressval  17294  ressress  17308  prdsval  17509  imasval  17566  imasaddvallem  17584  xpsfval  17621  xpsval  17625  cidval  17734  iscatd2  17738  oppcval  17770  ismon  17791  rescval  17885  idfucl  17939  funcres  17954  idfusubc0  17957  idfusubc  17958  fucval  18019  fucpropd  18038  setcval  18135  catcval  18158  estrcval  18181  xpcval  18234  1stfcl  18254  2ndfcl  18255  curf12  18284  curf2val  18287  curfcl  18289  hofcl  18316  oduval  18345  ipoval  18587  frmdval  18911  efmnd  18930  oppgval  19418  symgvalstruct  19468  efgmval  19783  efgmnvl  19785  efgi  19790  frgpup3lem  19848  dprd2da  20115  dmdprdpr  20122  dprdpr  20123  pgpfaclem1  20154  mgpval  20220  mgpress  20227  opprval  20421  sraval  21277  rlmval2  21294  pzriprnglem10  21621  zlmval  21646  znval  21666  znval2  21668  thlval  21826  islindf4  21969  psrval  22046  opsrval  22178  opsrval2  22180  matval  22549  mat1dimmul  22614  mat1dimcrng  22615  mat1scmat  22677  mdet0pr  22730  m1detdiag  22735  txkgen  23790  pt1hmeo  23944  xpstopnlem1  23947  xpstopnlem2  23949  tusval  24403  tmsval  24619  tngval  24777  om1val  25170  pi1xfrcnvlem  25196  pi1xfrcnv  25197  dchrval  27379  nosupbnd2lem1  27860  noinfbnd2lem1  27875  seqseq123d  28460  om2noseqrdg  28478  noseqrdgsuc  28482  ttgval  29205  eengv  29310  uspgr1ewop  29579  usgr2v1e2w  29583  1loopgruspgr  29831  1egrvtxdg1r  29841  1egrvtxdg0  29842  eupth2lem3lem3  30562  eupth2  30571  wlkl0  30699  br8d  32934  fresunsn  32951  elrgspnlem2  33544  rlocval  33560  rlocf1  33575  resvval  33630  opprabs  33745  idlsrgval  33774  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem1  33891  selvply1rhmlem3  33893  selvply1rhmlem5  33895  selvply1rhm  33896  mplidom  33899  extvfvcl  33907  resssra  33958  smatfval  34166  smatrcl  34167  smatlem  34168  qqhval  34343  bnj66  35229  bnj1234  35382  bnj1296  35390  bnj1450  35419  bnj1463  35424  bnj1501  35436  bnj1523  35440  subfacp1lem5  35657  cvmliftlem10  35767  cvmlift2lem12  35787  goaleq12d  35824  sategoelfvb  35892  msubffval  35996  msubfval  35997  elmsubrn  36001  msubrn  36002  msubco  36004  br8  36229  br6  36230  btwnouttr2  36495  brfs  36552  btwnconn1lem11  36570  cbvoprab3davw  36766  bj-dfid2ALT  37682  bj-endval  37940  csbfinxpg  38015  finixpnum  38237  ldualset  39880  tgrpfset  41499  tgrpset  41500  erngfset  41554  erngset  41555  erngfset-rN  41562  erngset-rN  41563  dvafset  41759  dvaset  41760  dvhfset  41835  dvhset  41836  dvhfvadd  41846  dvhopvadd2  41849  dib1dim2  41923  dicvscacl  41946  cdlemn6  41957  dihopelvalcpre  42003  dih1dimatlem  42084  hdmapfval  42582  hlhilset  42689  mendval  43889  mnringvald  44920  ovolval4lem1  47346  ovolval4lem2  47347  ovnovollem3  47355  isubgrvtxuhgr  48612  isubgr0uhgr  48621  stgrfv  48701  gpgov  48790  gpgprismgriedgdmss  48800  gpgvtx0  48801  gpgvtx1  48802  gpgedgvtx0  48809  gpgedgvtx1  48810  gpgvtxedg0  48811  gpgvtxedg1  48812  gpgedgiov  48813  gpgedg2ov  48814  gpgedg2iv  48815  gpg3kgrtriexlem6  48836  gpg3kgrtriex  48837  gpgprismgr4cycllem3  48845  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2  48865  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5  48871  gpg5edgnedg  48878  rngcvalALTV  49013  ringcvalALTV  49037  zlmodzxzsub  49123  lmod1zr  49256  2arymaptf  49415  discsubc  49825  2oppf  49893  upfval2  49938  upfval3  49939  isuplem  49940  uptpos  49959  uptr2  49982  dfswapf2  50022  oppc1stf  50049  oppc2ndf  50050  fucolid  50122  fucorid  50123  precofval2  50130  prcofval  50139  isinito2lem  50259  termcfuncval  50293  prstcval  50312  mndtcval  50340  lanup  50402  coccom  50425  iscmd  50427