Theorem opeq1d 4903

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

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  oteq1  4906  oteq2  4907  opth  5496  elsnxp  6322  cbvoprab2  7538  cbvoprab12v  7540  fvproj  8175  unxpdomlem1  9313  djulf1o  9981  djurf1o  9982  mulcanenq  11029  ax1rid  11230  axrnegex  11231  fseq1m1p1  13659  uzrdglem  14008  pfxswrd  14754  swrdccat  14783  swrdccat3blem  14787  cshw0  14842  cshwmodn  14843  s2prop  14956  s4prop  14959  fsum2dlem  15818  fprod2dlem  16028  ruclem1  16279  imasaddvallem  17589  iscatd2  17739  moni  17797  homadmcd  18109  curf1  18295  curf1cl  18298  curf2  18299  hofcl  18329  gsum2dlem2  20013  pzriprnglem10  21524  imasdsf1olem  24404  ovoliunlem1  25556  cxpcn3  26809  nosupbnd2  27779  noinfbnd2  27794  noseqrdglem  28329  axlowdimlem15  28989  axlowdim  28994  nvi  30646  nvop  30708  phop  30850  br8d  32632  fgreu  32690  1stpreimas  32717  rlocval  33231  rloccring  33242  smatfval  33741  smatrcl  33742  smatlem  33743  fmla0xp  35351  mvhfval  35501  mpst123  35508  br8  35718  fvtransport  35996  cbvoprab1vw  36203  cbvoprab2vw  36204  cbvoprab1davw  36237  cbvoprab2davw  36238  cbvoprab12davw  36241  bj-inftyexpitaudisj  37171  rfovcnvf1od  43966