Theorem opeq1d 4835

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  oteq1  4838  oteq2  4839  opth  5424  elsnxp  6249  cbvoprab2  7446  cbvoprab12v  7448  fvproj  8076  unxpdomlem1  9156  djulf1o  9824  djurf1o  9825  mulcanenq  10871  ax1rid  11072  axrnegex  11073  fseq1m1p1  13515  uzrdglem  13880  pfxswrd  14629  swrdccat  14658  swrdccat3blem  14662  cshw0  14717  cshwmodn  14718  s2prop  14830  s4prop  14833  fsum2dlem  15693  fprod2dlem  15903  ruclem1  16156  imasaddvallem  17450  iscatd2  17604  moni  17660  homadmcd  17966  curf1  18148  curf1cl  18151  curf2  18152  hofcl  18182  gsum2dlem2  19900  pzriprnglem10  21445  imasdsf1olem  24317  ovoliunlem1  25459  cxpcn3  26714  nosupbnd2  27684  noinfbnd2  27699  noseqrdglem  28301  axlowdimlem15  29029  axlowdim  29034  nvi  30689  nvop  30751  phop  30893  br8d  32686  fgreu  32750  1stpreimas  32785  rlocval  33341  rloccring  33352  smatfval  33952  smatrcl  33953  smatlem  33954  fmla0xp  35577  mvhfval  35727  mpst123  35734  br8  35950  fvtransport  36226  cbvoprab1vw  36431  cbvoprab2vw  36432  cbvoprab1davw  36465  cbvoprab2davw  36466  cbvoprab12davw  36469  bj-inftyexpitaudisj  37410  rfovcnvf1od  44245  oppcup3lem  49451  tposcurf2val  49546  oppcthinendcALT  49686  concom  49908