Theorem opeq1d 4439

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

Syntax hints:   → wi 4   = wceq 1523  ⟨cop 4216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217

This theorem is referenced by:  oteq1  4442  oteq2  4443  opth  4974  elsnxp  5715  cbvoprab2  6770  unxpdomlem1  8205  mulcanenq  9820  ax1rid  10020  axrnegex  10021  fseq1m1p1  12453  uzrdglem  12796  swrd0swrd  13507  swrdccat  13539  swrdccat3a  13540  swrdccat3blem  13541  cshw0  13586  cshwmodn  13587  s2prop  13698  s4prop  13701  fsum2dlem  14545  fprod2dlem  14754  ruclem1  15004  imasaddvallem  16236  iscatd2  16389  moni  16443  homadmcd  16739  curf1  16912  curf1cl  16915  curf2  16916  hofcl  16946  gsum2dlem2  18416  imasdsf1olem  22225  ovoliunlem1  23316  cxpcn3  24534  axlowdimlem15  25881  axlowdim  25886  nvi  27597  nvop  27659  phop  27801  br8d  29548  fgreu  29599  1stpreimas  29611  smatfval  29989  smatrcl  29990  smatlem  29991  fvproj  30027  mvhfval  31556  mpst123  31563  br8  31772  nosupbnd2  31987  fvtransport  32264  rfovcnvf1od  38615