Theorem opeq1d 4642

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

Syntax hints:   → wi 4   = wceq 1601  ⟨cop 4404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405

This theorem is referenced by:  oteq1  4645  oteq2  4646  opth  5176  elsnxp  5931  cbvoprab2  7005  unxpdomlem1  8452  djulf1o  9071  djurf1o  9072  mulcanenq  10117  ax1rid  10318  axrnegex  10319  fseq1m1p1  12733  uzrdglem  13075  swrd0swrdOLD  13815  pfxswrd  13816  swrdccat  13865  swrdccatOLD  13866  swrdccat3aOLD  13870  swrdccat3blem  13871  cshw0  13945  cshwmodn  13946  s2prop  14058  s4prop  14061  fsum2dlem  14906  fprod2dlem  15113  ruclem1  15364  imasaddvallem  16575  iscatd2  16727  moni  16781  homadmcd  17077  curf1  17251  curf1cl  17254  curf2  17255  hofcl  17285  gsum2dlem2  18756  imasdsf1olem  22586  ovoliunlem1  23706  cxpcn3  24929  axlowdimlem15  26305  axlowdim  26310  nvi  28041  nvop  28103  phop  28245  br8d  29985  fgreu  30037  1stpreimas  30049  smatfval  30459  smatrcl  30460  smatlem  30461  fvproj  30497  mvhfval  32029  mpst123  32036  br8  32240  nosupbnd2  32451  fvtransport  32728  bj-inftyexpitaudisj  33682  rfovcnvf1od  39254