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 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  dfid2  5547  funopsn  7152  funopsnOLD  7153  fmptsng  7174  fmptsnd  7175  fvproj  8154  tfrlem11  8400  seqomlem0  8463  seqomlem1  8464  seqomlem4  8467  seqomeq12  8468  fundmen  9063  dif1en  9181  unxpdomlem1  9251  mulcanenq  11049  elreal2  11221  om2uzrdg  14103  uzrdgsuci  14107  seqeq2  14152  seqeq3  14153  s1val  14749  s1eq  14751  swrdlsw  14822  pfxpfx  14862  swrdccat  14889  swrdccat3blem  14893  swrdccat3b  14894  pfxccatin12d  14899  swrds2  15097  swrds2m  15098  swrd2lsw  15111  eucalgval  16763  setsidvald  17383  ressval  17417  ressress  17431  prdsval  17632  imasval  17689  imasaddvallem  17707  xpsfval  17744  xpsval  17748  cidval  17857  iscatd2  17861  oppcval  17893  ismon  17914  rescval  18008  idfucl  18062  funcres  18077  idfusubc0  18080  idfusubc  18081  fucval  18142  fucpropd  18161  setcval  18258  catcval  18281  estrcval  18304  xpcval  18357  1stfcl  18377  2ndfcl  18378  curf12  18407  curf2val  18410  curfcl  18412  hofcl  18439  oduval  18468  ipoval  18710  frmdval  19053  efmnd  19072  oppgval  19567  symgvalstruct  19617  efgmval  19932  efgmnvl  19934  efgi  19939  frgpup3lem  19997  dprd2da  20264  dmdprdpr  20271  dprdpr  20272  pgpfaclem1  20303  mgpval  20369  mgpress  20376  opprval  20574  sraval  21456  rlmval2  21473  pzriprnglem10  21802  zlmval  21827  znval  21847  znval2  21849  thlval  22007  islindf4  22150  psrval  22229  opsrval  22361  opsrval2  22363  matval  22732  mat1dimmul  22797  mat1dimcrng  22798  mat1scmat  22860  mdet0pr  22913  m1detdiag  22918  txkgen  23977  pt1hmeo  24131  xpstopnlem1  24134  xpstopnlem2  24136  tusval  24590  tmsval  24806  tngval  24964  om1val  25357  pi1xfrcnvlem  25383  pi1xfrcnv  25384  dchrval  27567  nosupbnd2lem1  28078  noinfbnd2lem1  28093  seqseq123d  28678  om2noseqrdg  28696  noseqrdgsuc  28700  angmgmval  29400  ttgval  29458  eengv  29563  uspgr1ewop  29835  usgr2v1e2w  29839  1loopgruspgr  30087  1egrvtxdg1r  30097  1egrvtxdg0  30098  eupth2lem3lem3  30837  eupth2  30846  wlkl0  30974  br8d  33250  fresunsn  33267  elrgspnlem2  33851  rlocval  33867  rlocf1  33882  resvval  33937  opprabs  34053  idlsrgval  34082  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem1  34199  selvply1rhmlem3  34201  selvply1rhmlem5  34203  selvply1rhm  34204  mplidom  34207  extvfvcl  34215  resssra  34266  smatfval  34474  smatrcl  34475  smatlem  34476  qqhval  34651  bnj66  35537  bnj1234  35690  bnj1296  35698  bnj1450  35727  bnj1463  35732  bnj1501  35744  bnj1523  35748  subfacp1lem5  36036  cvmliftlem10  36146  cvmlift2lem12  36166  goaleq12d  36203  sategoelfvb  36271  msubffval  36375  msubfval  36376  elmsubrn  36380  msubrn  36381  msubco  36383  br8  36614  br6  36615  btwnouttr2  36880  brfs  36937  btwnconn1lem11  36955  cbvoprab3davw  37155  bj-dfid2ALT  38073  bj-endval  38330  csbfinxpg  38405  finixpnum  38622  ldualset  40276  tgrpfset  41895  tgrpset  41896  erngfset  41950  erngset  41951  erngfset-rN  41958  erngset-rN  41959  dvafset  42155  dvaset  42156  dvhfset  42231  dvhset  42232  dvhfvadd  42242  dvhopvadd2  42245  dib1dim2  42319  dicvscacl  42342  cdlemn6  42353  dihopelvalcpre  42399  dih1dimatlem  42480  hdmapfval  42978  hlhilset  43085  mendval  44275  mnringvald  45305  ovolval4lem1  47753  ovolval4lem2  47754  ovnovollem3  47762  isubgrvtxuhgr  49056  isubgr0uhgr  49065  stgrfv  49145  gpgov  49234  gpgprismgriedgdmss  49244  gpgvtx0  49245  gpgvtx1  49246  gpgedgvtx0  49253  gpgedgvtx1  49254  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  gpgedg2ov  49258  gpgedg2iv  49259  gpg3kgrtriexlem6  49280  gpg3kgrtriex  49281  gpgprismgr4cycllem3  49289  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5  49315  gpg5edgnedg  49322  rngcvalALTV  49456  ringcvalALTV  49480  zlmodzxzsub  49566  lmod1zr  49699  2arymaptf  49858  discsubc  50272  2oppf  50342  upfval2  50387  upfval3  50388  isuplem  50389  uptpos  50408  uptr2  50431  dfswapf2  50477  oppc1stf  50504  oppc2ndf  50505  fucolid  50577  fucorid  50578  precofval2  50598  prcofval  50607  isinito2lem  50727  termcfuncval  50761  termcfunc1eq  50764  prstcval  50783  mndtcval  50811  lanup  50918  coccom  50941  iscmd  50943