Theorem opeq1d 4831

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583

This theorem is referenced by:  oteq1  4834  oteq2  4835  opth  5416  elsnxp  6238  cbvoprab2  7434  cbvoprab12v  7436  fvproj  8064  unxpdomlem1  9140  djulf1o  9805  djurf1o  9806  mulcanenq  10851  ax1rid  11052  axrnegex  11053  fseq1m1p1  13499  uzrdglem  13864  pfxswrd  14613  swrdccat  14642  swrdccat3blem  14646  cshw0  14701  cshwmodn  14702  s2prop  14814  s4prop  14817  fsum2dlem  15677  fprod2dlem  15887  ruclem1  16140  imasaddvallem  17433  iscatd2  17587  moni  17643  homadmcd  17949  curf1  18131  curf1cl  18134  curf2  18135  hofcl  18165  gsum2dlem2  19884  pzriprnglem10  21428  imasdsf1olem  24289  ovoliunlem1  25431  cxpcn3  26686  nosupbnd2  27656  noinfbnd2  27671  noseqrdglem  28236  axlowdimlem15  28935  axlowdim  28940  nvi  30592  nvop  30654  phop  30796  br8d  32589  fgreu  32652  1stpreimas  32685  rlocval  33224  rloccring  33235  smatfval  33806  smatrcl  33807  smatlem  33808  fmla0xp  35425  mvhfval  35575  mpst123  35582  br8  35798  fvtransport  36072  cbvoprab1vw  36277  cbvoprab2vw  36278  cbvoprab1davw  36311  cbvoprab2davw  36312  cbvoprab12davw  36315  bj-inftyexpitaudisj  37245  rfovcnvf1od  44043  oppcup3lem  49244  tposcurf2val  49339  oppcthinendcALT  49479  concom  49701