Theorem opeq2d 4835

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  dfid2  5540  funopsn  7125  funopsnOLD  7126  fmptsng  7147  fmptsnd  7148  fvproj  8108  tfrlem11  8353  seqomlem0  8414  seqomlem1  8415  seqomlem4  8418  seqomeq12  8419  fundmen  9006  dif1en  9124  unxpdomlem1  9194  mulcanenq  10912  elreal2  11084  om2uzrdg  13963  uzrdgsuci  13967  seqeq2  14012  seqeq3  14013  s1val  14606  s1eq  14608  swrdlsw  14675  pfxpfx  14715  swrdccat  14742  swrdccat3blem  14746  swrdccat3b  14747  pfxccatin12d  14752  swrds2  14947  swrds2m  14948  swrd2lsw  14959  eucalgval  16607  setsidvald  17226  ressval  17260  ressress  17274  prdsval  17475  imasval  17532  imasaddvallem  17550  xpsfval  17587  xpsval  17591  cidval  17700  iscatd2  17704  oppcval  17736  ismon  17757  rescval  17851  idfucl  17905  funcres  17920  idfusubc0  17923  idfusubc  17924  fucval  17985  fucpropd  18004  setcval  18101  catcval  18124  estrcval  18147  xpcval  18200  1stfcl  18220  2ndfcl  18221  curf12  18250  curf2val  18253  curfcl  18255  hofcl  18282  oduval  18311  ipoval  18553  frmdval  18876  efmnd  18895  oppgval  19378  symgvalstruct  19428  efgmval  19743  efgmnvl  19745  efgi  19750  frgpup3lem  19808  dprd2da  20075  dmdprdpr  20082  dprdpr  20083  pgpfaclem1  20114  mgpval  20180  mgpress  20187  opprval  20374  sraval  21230  rlmval2  21247  pzriprnglem10  21530  zlmval  21555  znval  21575  znval2  21577  thlval  21735  islindf4  21878  psrval  21955  opsrval  22087  opsrval2  22089  matval  22459  mat1dimmul  22524  mat1dimcrng  22525  mat1scmat  22587  mdet0pr  22640  m1detdiag  22645  txkgen  23700  pt1hmeo  23854  xpstopnlem1  23857  xpstopnlem2  23859  tusval  24313  tmsval  24529  tngval  24687  om1val  25080  pi1xfrcnvlem  25106  pi1xfrcnv  25107  dchrval  27286  nosupbnd2lem1  27767  noinfbnd2lem1  27782  seqseq123d  28367  om2noseqrdg  28385  noseqrdgsuc  28389  ttgval  29032  eengv  29137  uspgr1ewop  29406  usgr2v1e2w  29410  1loopgruspgr  29658  1egrvtxdg1r  29668  1egrvtxdg0  29669  eupth2lem3lem3  30389  eupth2  30398  wlkl0  30526  br8d  32771  fresunsn  32788  elrgspnlem2  33385  rlocval  33401  rlocf1  33416  resvval  33476  opprabs  33631  idlsrgval  33660  selvply1rhmlema  33776  selvply1rhmlemb  33777  selvply1rhmlem1  33778  selvply1rhmlem3  33780  selvply1rhmlem5  33782  selvply1rhm  33783  mplidom  33786  extvfvcl  33794  resssra  33845  smatfval  34053  smatrcl  34054  smatlem  34055  qqhval  34230  bnj66  35116  bnj1234  35269  bnj1296  35277  bnj1450  35306  bnj1463  35311  bnj1501  35323  bnj1523  35327  subfacp1lem5  35495  cvmliftlem10  35605  cvmlift2lem12  35625  goaleq12d  35662  sategoelfvb  35730  msubffval  35834  msubfval  35835  elmsubrn  35839  msubrn  35840  msubco  35842  br8  36067  br6  36068  btwnouttr2  36333  brfs  36390  btwnconn1lem11  36408  cbvoprab3davw  36594  bj-dfid2ALT  37511  bj-endval  37768  csbfinxpg  37843  finixpnum  38065  ldualset  39710  tgrpfset  41329  tgrpset  41330  erngfset  41384  erngset  41385  erngfset-rN  41392  erngset-rN  41393  dvafset  41589  dvaset  41590  dvhfset  41665  dvhset  41666  dvhfvadd  41676  dvhopvadd2  41679  dib1dim2  41753  dicvscacl  41776  cdlemn6  41787  dihopelvalcpre  41833  dih1dimatlem  41914  hdmapfval  42412  hlhilset  42519  mendval  43717  mnringvald  44750  ovolval4lem1  47184  ovolval4lem2  47185  ovnovollem3  47193  isubgrvtxuhgr  48447  isubgr0uhgr  48456  stgrfv  48536  gpgov  48625  gpgprismgriedgdmss  48635  gpgvtx0  48636  gpgvtx1  48637  gpgedgvtx0  48644  gpgedgvtx1  48645  gpgvtxedg0  48646  gpgvtxedg1  48647  gpgedgiov  48648  gpgedg2ov  48649  gpgedg2iv  48650  gpg3kgrtriexlem6  48671  gpg3kgrtriex  48672  gpgprismgr4cycllem3  48680  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem2  48700  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5  48706  gpg5edgnedg  48713  rngcvalALTV  48848  ringcvalALTV  48872  zlmodzxzsub  48943  lmod1zr  49076  2arymaptf  49235  discsubc  49646  2oppf  49714  upfval2  49759  upfval3  49760  isuplem  49761  uptpos  49780  uptr2  49803  dfswapf2  49843  oppc1stf  49870  oppc2ndf  49871  fucolid  49943  fucorid  49944  precofval2  49951  prcofval  49960  isinito2lem  50080  termcfuncval  50114  prstcval  50133  mndtcval  50161  lanup  50223  coccom  50246  iscmd  50248