Theorem opeq2d 4844

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

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

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  dfid2  5535  funopsn  7120  fmptsng  7142  fmptsnd  7143  fvproj  8113  tfrlem11  8356  seqomlem0  8417  seqomlem1  8418  seqomlem4  8421  seqomeq12  8422  fundmen  9002  dif1en  9124  dif1enOLD  9126  unxpdomlem1  9197  mulcanenq  10913  elreal2  11085  om2uzrdg  13921  uzrdgsuci  13925  seqeq2  13970  seqeq3  13971  s1val  14563  s1eq  14565  swrdlsw  14632  pfxpfx  14673  swrdccat  14700  swrdccat3blem  14704  swrdccat3b  14705  pfxccatin12d  14710  swrds2  14906  swrds2m  14907  swrd2lsw  14918  eucalgval  16552  setsidvald  17169  ressval  17203  ressress  17217  prdsval  17418  imasval  17474  imasaddvallem  17492  xpsfval  17529  xpsval  17533  cidval  17638  iscatd2  17642  oppcval  17674  ismon  17695  rescval  17789  idfucl  17843  funcres  17858  idfusubc0  17861  idfusubc  17862  fucval  17923  fucpropd  17942  setcval  18039  catcval  18062  estrcval  18085  xpcval  18138  1stfcl  18158  2ndfcl  18159  curf12  18188  curf2val  18191  curfcl  18193  hofcl  18220  oduval  18249  ipoval  18489  frmdval  18778  efmnd  18797  oppgval  19279  symgvalstruct  19327  efgmval  19642  efgmnvl  19644  efgi  19649  frgpup3lem  19707  dprd2da  19974  dmdprdpr  19981  dprdpr  19982  pgpfaclem1  20013  mgpval  20052  mgpress  20059  opprval  20247  sraval  21082  rlmval2  21099  pzriprnglem10  21400  zlmval  21425  znval  21445  znval2  21447  thlval  21604  islindf4  21747  psrval  21824  opsrval  21953  opsrval2  21955  matval  22298  mat1dimmul  22363  mat1dimcrng  22364  mat1scmat  22426  mdet0pr  22479  m1detdiag  22484  txkgen  23539  pt1hmeo  23693  xpstopnlem1  23696  xpstopnlem2  23698  tusval  24153  tmsval  24369  tngval  24527  om1val  24930  pi1xfrcnvlem  24956  pi1xfrcnv  24957  dchrval  27145  nosupbnd2lem1  27627  noinfbnd2lem1  27642  seqseq123d  28180  om2noseqrdg  28198  noseqrdgsuc  28202  ttgval  28802  eengv  28906  uspgr1ewop  29175  usgr2v1e2w  29179  1loopgruspgr  29428  1egrvtxdg1r  29438  1egrvtxdg0  29439  eupth2lem3lem3  30159  eupth2  30168  wlkl0  30296  br8d  32538  elrgspnlem2  33194  rlocval  33210  rlocf1  33224  resvval  33301  opprabs  33453  idlsrgval  33474  resssra  33583  smatfval  33785  smatrcl  33786  smatlem  33787  qqhval  33962  bnj66  34850  bnj1234  35003  bnj1296  35011  bnj1450  35040  bnj1463  35045  bnj1501  35057  bnj1523  35061  subfacp1lem5  35171  cvmliftlem10  35281  cvmlift2lem12  35301  goaleq12d  35338  sategoelfvb  35406  msubffval  35510  msubfval  35511  elmsubrn  35515  msubrn  35516  msubco  35518  br8  35743  br6  35744  btwnouttr2  36010  brfs  36067  btwnconn1lem11  36085  cbvoprab3davw  36261  bj-dfid2ALT  37053  bj-endval  37303  csbfinxpg  37376  finixpnum  37599  ldualset  39118  tgrpfset  40738  tgrpset  40739  erngfset  40793  erngset  40794  erngfset-rN  40801  erngset-rN  40802  dvafset  40998  dvaset  40999  dvhfset  41074  dvhset  41075  dvhfvadd  41085  dvhopvadd2  41088  dib1dim2  41162  dicvscacl  41185  cdlemn6  41196  dihopelvalcpre  41242  dih1dimatlem  41323  hdmapfval  41821  hlhilset  41928  mendval  43168  mnringvald  44202  ovolval4lem1  46647  ovolval4lem2  46648  ovnovollem3  46656  isubgrvtxuhgr  47864  isubgr0uhgr  47873  stgrfv  47952  gpgov  48033  gpgprismgriedgdmss  48043  gpgvtx0  48044  gpgvtx1  48045  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2ov  48057  gpgedg2iv  48058  gpg3kgrtriexlem6  48079  gpg3kgrtriex  48080  gpgprismgr4cycllem3  48087  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5  48113  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