Theorem opeq1d 4843

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  oteq1  4846  oteq2  4847  opth  5436  elsnxp  6264  cbvoprab2  7477  cbvoprab12v  7479  fvproj  8113  unxpdomlem1  9197  djulf1o  9865  djurf1o  9866  mulcanenq  10913  ax1rid  11114  axrnegex  11115  fseq1m1p1  13560  uzrdglem  13922  pfxswrd  14671  swrdccat  14700  swrdccat3blem  14704  cshw0  14759  cshwmodn  14760  s2prop  14873  s4prop  14876  fsum2dlem  15736  fprod2dlem  15946  ruclem1  16199  imasaddvallem  17492  iscatd2  17642  moni  17698  homadmcd  18004  curf1  18186  curf1cl  18189  curf2  18190  hofcl  18220  gsum2dlem2  19901  pzriprnglem10  21400  imasdsf1olem  24261  ovoliunlem1  25403  cxpcn3  26658  nosupbnd2  27628  noinfbnd2  27643  noseqrdglem  28199  axlowdimlem15  28883  axlowdim  28888  nvi  30543  nvop  30605  phop  30747  br8d  32538  fgreu  32596  1stpreimas  32629  rlocval  33210  rloccring  33221  smatfval  33785  smatrcl  33786  smatlem  33787  fmla0xp  35370  mvhfval  35520  mpst123  35527  br8  35743  fvtransport  36020  cbvoprab1vw  36225  cbvoprab2vw  36226  cbvoprab1davw  36259  cbvoprab2davw  36260  cbvoprab12davw  36263  bj-inftyexpitaudisj  37193  rfovcnvf1od  43993  oppcup3lem  49195  tposcurf2val  49290  oppcthinendcALT  49430  concom  49652