Theorem opeq1d 4764

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-un 3846  df-sn 4514  df-pr 4516  df-op 4520

This theorem is referenced by:  oteq1  4767  oteq2  4768  opth  5331  elsnxp  6117  cbvoprab2  7250  fvproj  7847  unxpdomlem1  8794  djulf1o  9407  djurf1o  9408  mulcanenq  10453  ax1rid  10654  axrnegex  10655  fseq1m1p1  13066  uzrdglem  13409  pfxswrd  14150  swrdccat  14179  swrdccat3blem  14183  cshw0  14238  cshwmodn  14239  s2prop  14351  s4prop  14354  fsum2dlem  15211  fprod2dlem  15419  ruclem1  15669  imasaddvallem  16898  iscatd2  17048  moni  17104  homadmcd  17407  curf1  17584  curf1cl  17587  curf2  17588  hofcl  17618  gsum2dlem2  19203  imasdsf1olem  23119  ovoliunlem1  24247  cxpcn3  25481  axlowdimlem15  26894  axlowdim  26899  nvi  28541  nvop  28603  phop  28745  br8d  30516  fgreu  30576  1stpreimas  30605  smatfval  31309  smatrcl  31310  smatlem  31311  fmla0xp  32908  mvhfval  33058  mpst123  33065  br8  33287  frxp3  33400  xpord3pred  33401  nosupbnd2  33552  noinfbnd2  33567  fvtransport  33964  bj-inftyexpitaudisj  34986  rfovcnvf1od  41142