Theorem opeq1d 4880

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

Syntax hints:   → wi 4   = wceq 1542  ⟨cop 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636

This theorem is referenced by:  oteq1  4883  oteq2  4884  opth  5477  elsnxp  6291  cbvoprab2  7497  fvproj  8120  unxpdomlem1  9250  djulf1o  9907  djurf1o  9908  mulcanenq  10955  ax1rid  11156  axrnegex  11157  fseq1m1p1  13576  uzrdglem  13922  pfxswrd  14656  swrdccat  14685  swrdccat3blem  14689  cshw0  14744  cshwmodn  14745  s2prop  14858  s4prop  14861  fsum2dlem  15716  fprod2dlem  15924  ruclem1  16174  imasaddvallem  17475  iscatd2  17625  moni  17683  homadmcd  17992  curf1  18178  curf1cl  18181  curf2  18182  hofcl  18212  gsum2dlem2  19839  imasdsf1olem  23879  ovoliunlem1  25019  cxpcn3  26256  nosupbnd2  27219  noinfbnd2  27234  axlowdimlem15  28245  axlowdim  28250  nvi  29898  nvop  29960  phop  30102  br8d  31870  fgreu  31928  1stpreimas  31958  smatfval  32806  smatrcl  32807  smatlem  32808  fmla0xp  34405  mvhfval  34555  mpst123  34562  br8  34757  fvtransport  35035  bj-inftyexpitaudisj  36134  rfovcnvf1od  42803  pzriprnglem10  46862