Theorem opeq1d 4879

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  oteq1  4882  oteq2  4883  opth  5481  elsnxp  6311  cbvoprab2  7521  cbvoprab12v  7523  fvproj  8159  unxpdomlem1  9286  djulf1o  9952  djurf1o  9953  mulcanenq  11000  ax1rid  11201  axrnegex  11202  fseq1m1p1  13639  uzrdglem  13998  pfxswrd  14744  swrdccat  14773  swrdccat3blem  14777  cshw0  14832  cshwmodn  14833  s2prop  14946  s4prop  14949  fsum2dlem  15806  fprod2dlem  16016  ruclem1  16267  imasaddvallem  17574  iscatd2  17724  moni  17780  homadmcd  18087  curf1  18270  curf1cl  18273  curf2  18274  hofcl  18304  gsum2dlem2  19989  pzriprnglem10  21501  imasdsf1olem  24383  ovoliunlem1  25537  cxpcn3  26791  nosupbnd2  27761  noinfbnd2  27776  noseqrdglem  28311  axlowdimlem15  28971  axlowdim  28976  nvi  30633  nvop  30695  phop  30837  br8d  32622  fgreu  32682  1stpreimas  32715  rlocval  33263  rloccring  33274  smatfval  33794  smatrcl  33795  smatlem  33796  fmla0xp  35388  mvhfval  35538  mpst123  35545  br8  35756  fvtransport  36033  cbvoprab1vw  36238  cbvoprab2vw  36239  cbvoprab1davw  36272  cbvoprab2davw  36273  cbvoprab12davw  36276  bj-inftyexpitaudisj  37206  rfovcnvf1od  44017  tposcurf2val  49001  oppcthinendcALT  49090