Theorem opeq1d 4832

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

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

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584

This theorem is referenced by:  oteq1  4835  oteq2  4836  opth  5421  elsnxp  6245  cbvoprab2  7442  cbvoprab12v  7444  fvproj  8072  unxpdomlem1  9149  djulf1o  9814  djurf1o  9815  mulcanenq  10860  ax1rid  11061  axrnegex  11062  fseq1m1p1  13503  uzrdglem  13868  pfxswrd  14617  swrdccat  14646  swrdccat3blem  14650  cshw0  14705  cshwmodn  14706  s2prop  14818  s4prop  14821  fsum2dlem  15681  fprod2dlem  15891  ruclem1  16144  imasaddvallem  17437  iscatd2  17591  moni  17647  homadmcd  17953  curf1  18135  curf1cl  18138  curf2  18139  hofcl  18169  gsum2dlem2  19887  pzriprnglem10  21431  imasdsf1olem  24291  ovoliunlem1  25433  cxpcn3  26688  nosupbnd2  27658  noinfbnd2  27673  noseqrdglem  28238  axlowdimlem15  28938  axlowdim  28943  nvi  30598  nvop  30660  phop  30802  br8d  32595  fgreu  32658  1stpreimas  32693  rlocval  33235  rloccring  33246  smatfval  33831  smatrcl  33832  smatlem  33833  fmla0xp  35450  mvhfval  35600  mpst123  35607  br8  35823  fvtransport  36099  cbvoprab1vw  36304  cbvoprab2vw  36305  cbvoprab1davw  36338  cbvoprab2davw  36339  cbvoprab12davw  36342  bj-inftyexpitaudisj  37272  rfovcnvf1od  44124  oppcup3lem  49334  tposcurf2val  49429  oppcthinendcALT  49569  concom  49791