MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq2d Structured version   Visualization version   GIF version

Theorem opeq2d 4775
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
StepHypRef Expression
1 opeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 opeq2 4768 . 2 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
31, 2syl 17 1 (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cop 4534
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535
This theorem is referenced by:  funopsn  6891  fmptsng  6911  fmptsnd  6912  fvproj  7815  tfrlem11  8011  seqomlem0  8072  seqomlem1  8073  seqomlem4  8076  seqomeq12  8077  fundmen  8570  unxpdomlem1  8710  mulcanenq  10375  elreal2  10547  om2uzrdg  13323  uzrdgsuci  13327  seqeq2  13372  seqeq3  13373  s1val  13947  s1eq  13949  swrdlsw  14024  pfxpfx  14065  swrdccat  14092  swrdccat3blem  14096  swrdccat3b  14097  pfxccatin12d  14102  swrds2  14297  swrds2m  14298  swrd2lsw  14309  eucalgval  15920  setsidvald  16510  ressval  16547  ressress  16558  prdsval  16724  imasval  16780  imasaddvallem  16798  xpsfval  16835  xpsval  16839  cidval  16944  iscatd2  16948  oppcval  16979  ismon  16999  rescval  17093  idfucl  17147  funcres  17162  fucval  17224  fucpropd  17243  setcval  17333  catcval  17352  estrcval  17370  xpcval  17423  1stfcl  17443  2ndfcl  17444  curf12  17473  curf2val  17476  curfcl  17478  hofcl  17505  oduval  17736  ipoval  17760  frmdval  18012  efmnd  18031  oppgval  18471  symgvalstruct  18521  efgmval  18834  efgmnvl  18836  efgi  18841  frgpup3lem  18899  dprd2da  19161  dmdprdpr  19168  dprdpr  19169  pgpfaclem1  19200  mgpval  19239  mgpress  19247  opprval  19374  sraval  19945  rlmval2  19963  zlmval  20213  znval  20231  znval2  20233  thlval  20388  islindf4  20531  psrval  20604  opsrval  20718  opsrval2  20720  matval  21020  mat1dimmul  21085  mat1dimcrng  21086  mat1scmat  21148  mdet0pr  21201  m1detdiag  21206  txkgen  22261  pt1hmeo  22415  xpstopnlem1  22418  xpstopnlem2  22420  tusval  22876  tmsval  23092  tngval  23249  om1val  23639  pi1xfrcnvlem  23665  pi1xfrcnv  23666  dchrval  25822  ttgval  26673  eengv  26777  uspgr1ewop  27042  usgr2v1e2w  27046  1loopgruspgr  27294  1egrvtxdg1r  27304  1egrvtxdg0  27305  eupth2lem3lem3  28019  eupth2  28028  wlkl0  28156  br8d  30378  resvval  30955  idlsrgval  31060  smatfval  31152  smatrcl  31153  smatlem  31154  qqhval  31329  bnj66  32246  bnj1234  32399  bnj1296  32407  bnj1450  32436  bnj1463  32441  bnj1501  32453  bnj1523  32457  subfacp1lem5  32545  cvmliftlem10  32655  cvmlift2lem12  32675  goaleq12d  32712  sategoelfvb  32780  msubffval  32884  msubfval  32885  elmsubrn  32889  msubrn  32890  msubco  32892  br8  33106  br6  33107  nosupbnd2lem1  33329  btwnouttr2  33597  brfs  33654  btwnconn1lem11  33672  bj-endval  34730  csbfinxpg  34806  finixpnum  35041  ldualset  36420  tgrpfset  38039  tgrpset  38040  erngfset  38094  erngset  38095  erngfset-rN  38102  erngset-rN  38103  dvafset  38299  dvaset  38300  dvhfset  38375  dvhset  38376  dvhfvadd  38386  dvhopvadd2  38389  dib1dim2  38463  dicvscacl  38486  cdlemn6  38497  dihopelvalcpre  38543  dih1dimatlem  38624  hdmapfval  39122  hlhilset  39229  mendval  40120  mnringvald  40914  ovolval4lem1  43281  ovolval4lem2  43282  ovnovollem3  43290  idfusubc0  44482  idfusubc  44483  rngcvalALTV  44578  ringcvalALTV  44624  zlmodzxzsub  44755  lmod1zr  44895  2arymaptf  45059
  Copyright terms: Public domain W3C validator