Theorem opeq1d 4849

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4600

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is used by:  oteq1  4852  oteq2  4853  opth  5463  elsnxp  6299  cbvoprab2  7511  cbvoprab12v  7513  fvproj  8139  unxpdomlem1  9226  djulf1o  9917  djurf1o  9918  mulcanenq  10963  ax1rid  11164  axrnegex  11165  fseq1m1p1  13646  uzrdglem  14013  pfxswrd  14767  swrdccat  14796  swrdccat3blem  14800  cshw0  14857  cshwmodn  14858  s2prop  14970  s4prop  14973  fsum2dlem  15847  fprod2dlem  16060  ruclem1  16312  imasaddvallem  17608  iscatd2  17762  moni  17818  homadmcd  18124  curf1  18306  curf1cl  18309  curf2  18310  hofcl  18340  gsum2dlem2  20072  pzriprnglem10  21677  imasdsf1olem  24567  ovoliunlem1  25698  cxpcn3  26950  nosupbnd2  27917  noinfbnd2  27932  noseqrdglem  28535  axlowdimlem15  29343  axlowdim  29348  nvi  31003  nvop  31065  phop  31207  br8d  32990  fgreu  33053  1stpreimas  33088  rlocval  33610  rloccring  33622  smatfval  34216  smatrcl  34217  smatlem  34218  fmla0xp  35896  mvhfval  36046  mpst123  36053  br8  36269  fvtransport  36545  cbvoprab1vw  36790  cbvoprab2vw  36791  cbvoprab1davw  36824  cbvoprab2davw  36825  cbvoprab12davw  36828  bj-inftyexpitaudisj  37890  rfovcnvf1od  44771  oppcup3lem  50025  tposcurf2val  50120  oppcthinendcALT  50260  concom  50482