Theorem opeq1d 4846

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  oteq1  4849  oteq2  4850  opth  5439  elsnxp  6267  cbvoprab2  7480  cbvoprab12v  7482  fvproj  8116  unxpdomlem1  9204  djulf1o  9872  djurf1o  9873  mulcanenq  10920  ax1rid  11121  axrnegex  11122  fseq1m1p1  13567  uzrdglem  13929  pfxswrd  14678  swrdccat  14707  swrdccat3blem  14711  cshw0  14766  cshwmodn  14767  s2prop  14880  s4prop  14883  fsum2dlem  15743  fprod2dlem  15953  ruclem1  16206  imasaddvallem  17499  iscatd2  17649  moni  17705  homadmcd  18011  curf1  18193  curf1cl  18196  curf2  18197  hofcl  18227  gsum2dlem2  19908  pzriprnglem10  21407  imasdsf1olem  24268  ovoliunlem1  25410  cxpcn3  26665  nosupbnd2  27635  noinfbnd2  27650  noseqrdglem  28206  axlowdimlem15  28890  axlowdim  28895  nvi  30550  nvop  30612  phop  30754  br8d  32545  fgreu  32603  1stpreimas  32636  rlocval  33217  rloccring  33228  smatfval  33792  smatrcl  33793  smatlem  33794  fmla0xp  35377  mvhfval  35527  mpst123  35534  br8  35750  fvtransport  36027  cbvoprab1vw  36232  cbvoprab2vw  36233  cbvoprab1davw  36266  cbvoprab2davw  36267  cbvoprab12davw  36270  bj-inftyexpitaudisj  37200  rfovcnvf1od  44000  oppcup3lem  49199  tposcurf2val  49294  oppcthinendcALT  49434  concom  49656