Theorem opeq2d 4840

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  dfid2  5552  funopsn  7144  funopsnOLD  7145  fmptsng  7166  fmptsnd  7167  fvproj  8132  tfrlem11  8377  seqomlem0  8438  seqomlem1  8439  seqomlem4  8442  seqomeq12  8443  fundmen  9038  dif1en  9156  unxpdomlem1  9226  mulcanenq  10969  elreal2  11141  om2uzrdg  14020  uzrdgsuci  14024  seqeq2  14069  seqeq3  14070  s1val  14665  s1eq  14667  swrdlsw  14737  pfxpfx  14777  swrdccat  14804  swrdccat3blem  14808  swrdccat3b  14809  pfxccatin12d  14814  swrds2  15011  swrds2m  15012  swrd2lsw  15025  eucalgval  16672  setsidvald  17291  ressval  17325  ressress  17339  prdsval  17540  imasval  17597  imasaddvallem  17615  xpsfval  17652  xpsval  17656  cidval  17765  iscatd2  17769  oppcval  17801  ismon  17822  rescval  17916  idfucl  17970  funcres  17985  idfusubc0  17988  idfusubc  17989  fucval  18050  fucpropd  18069  setcval  18166  catcval  18189  estrcval  18212  xpcval  18265  1stfcl  18285  2ndfcl  18286  curf12  18315  curf2val  18318  curfcl  18320  hofcl  18347  oduval  18376  ipoval  18618  frmdval  18960  efmnd  18979  oppgval  19474  symgvalstruct  19524  efgmval  19839  efgmnvl  19841  efgi  19846  frgpup3lem  19904  dprd2da  20171  dmdprdpr  20178  dprdpr  20179  pgpfaclem1  20210  mgpval  20276  mgpress  20283  opprval  20479  sraval  21359  rlmval2  21376  pzriprnglem10  21703  zlmval  21728  znval  21748  znval2  21750  thlval  21908  islindf4  22051  psrval  22130  opsrval  22262  opsrval2  22264  matval  22633  mat1dimmul  22698  mat1dimcrng  22699  mat1scmat  22761  mdet0pr  22814  m1detdiag  22819  txkgen  23878  pt1hmeo  24032  xpstopnlem1  24035  xpstopnlem2  24037  tusval  24491  tmsval  24707  tngval  24865  om1val  25258  pi1xfrcnvlem  25284  pi1xfrcnv  25285  dchrval  27470  nosupbnd2lem1  27951  noinfbnd2lem1  27966  seqseq123d  28551  om2noseqrdg  28569  noseqrdgsuc  28573  angmgmval  29273  ttgval  29331  eengv  29436  uspgr1ewop  29708  usgr2v1e2w  29712  1loopgruspgr  29960  1egrvtxdg1r  29970  1egrvtxdg0  29971  eupth2lem3lem3  30710  eupth2  30719  wlkl0  30847  br8d  33081  fresunsn  33098  elrgspnlem2  33683  rlocval  33699  rlocf1  33714  resvval  33769  opprabs  33884  idlsrgval  33913  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem3  34032  selvply1rhmlem5  34034  selvply1rhm  34035  mplidom  34038  extvfvcl  34046  resssra  34097  smatfval  34305  smatrcl  34306  smatlem  34307  qqhval  34482  bnj66  35369  bnj1234  35522  bnj1296  35530  bnj1450  35559  bnj1463  35564  bnj1501  35576  bnj1523  35580  subfacp1lem5  35763  cvmliftlem10  35873  cvmlift2lem12  35893  goaleq12d  35930  sategoelfvb  35998  msubffval  36102  msubfval  36103  elmsubrn  36107  msubrn  36108  msubco  36110  br8  36335  br6  36336  btwnouttr2  36602  brfs  36659  btwnconn1lem11  36677  cbvoprab3davw  36893  bj-dfid2ALT  37809  bj-endval  38067  csbfinxpg  38142  finixpnum  38359  ldualset  39998  tgrpfset  41617  tgrpset  41618  erngfset  41672  erngset  41673  erngfset-rN  41680  erngset-rN  41681  dvafset  41877  dvaset  41878  dvhfset  41953  dvhset  41954  dvhfvadd  41964  dvhopvadd2  41967  dib1dim2  42041  dicvscacl  42064  cdlemn6  42075  dihopelvalcpre  42121  dih1dimatlem  42202  hdmapfval  42700  hlhilset  42807  mendval  44020  mnringvald  45051  ovolval4lem1  47477  ovolval4lem2  47478  ovnovollem3  47486  isubgrvtxuhgr  48780  isubgr0uhgr  48789  stgrfv  48869  gpgov  48958  gpgprismgriedgdmss  48968  gpgvtx0  48969  gpgvtx1  48970  gpgedgvtx0  48977  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  gpg3kgrtriexlem6  49004  gpg3kgrtriex  49005  gpgprismgr4cycllem3  49013  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5  49039  gpg5edgnedg  49046  rngcvalALTV  49180  ringcvalALTV  49204  zlmodzxzsub  49290  lmod1zr  49423  2arymaptf  49582  discsubc  49990  2oppf  50058  upfval2  50103  upfval3  50104  isuplem  50105  uptpos  50124  uptr2  50147  dfswapf2  50187  oppc1stf  50214  oppc2ndf  50215  fucolid  50287  fucorid  50288  precofval2  50295  prcofval  50304  isinito2lem  50424  termcfuncval  50458  prstcval  50477  mndtcval  50505  lanup  50567  coccom  50590  iscmd  50592