Theorem opeq1d 4839

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq1d	⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq1 4833	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
3	1, 2	syl 18	1 ⊢ (𝜑 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   = wceq 1563  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  oteq1  4842  oteq2  4843  opth  5448  elsnxp  6281  cbvoprab2  7488  cbvoprab12v  7490  fvproj  8118  unxpdomlem1  9204  djulf1o  9886  djurf1o  9887  mulcanenq  10933  ax1rid  11134  axrnegex  11135  fseq1m1p1  13615  uzrdglem  13981  pfxswrd  14731  swrdccat  14760  swrdccat3blem  14764  cshw0  14819  cshwmodn  14820  s2prop  14932  s4prop  14935  fsum2dlem  15809  fprod2dlem  16022  ruclem1  16275  imasaddvallem  17571  iscatd2  17725  moni  17781  homadmcd  18087  curf1  18269  curf1cl  18272  curf2  18273  hofcl  18303  gsum2dlem2  20029  pzriprnglem10  21597  imasdsf1olem  24487  ovoliunlem1  25618  cxpcn3  26867  nosupbnd2  27834  noinfbnd2  27849  noseqrdglem  28452  axlowdimlem15  29211  axlowdim  29216  nvi  30871  nvop  30933  phop  31075  br8d  32861  fgreu  32924  1stpreimas  32959  rlocval  33487  rloccring  33499  smatfval  34097  smatrcl  34098  smatlem  34099  fmla0xp  35741  mvhfval  35891  mpst123  35898  br8  36114  fvtransport  36390  cbvoprab1vw  36605  cbvoprab2vw  36606  cbvoprab1davw  36639  cbvoprab2davw  36640  cbvoprab12davw  36643  bj-inftyexpitaudisj  37704  rfovcnvf1od  44587  oppcup3lem  49836  tposcurf2val  49931  oppcthinendcALT  50071  concom  50293