Theorem opeq1d 4817

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

Syntax hints:   → wi 4   = wceq 1547  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  oteq1  4820  oteq2  4821  opth  5423  elsnxp  6249  cbvoprab2  7451  cbvoprab12v  7453  fvproj  8081  unxpdomlem1  9163  djulf1o  9834  djurf1o  9835  mulcanenq  10881  ax1rid  11082  axrnegex  11083  fseq1m1p1  13551  uzrdglem  13917  pfxswrd  14666  swrdccat  14695  swrdccat3blem  14699  cshw0  14754  cshwmodn  14755  s2prop  14867  s4prop  14870  fsum2dlem  15730  fprod2dlem  15943  ruclem1  16196  imasaddvallem  17491  iscatd2  17645  moni  17701  homadmcd  18007  curf1  18189  curf1cl  18192  curf2  18193  hofcl  18223  gsum2dlem2  19944  pzriprnglem10  21472  imasdsf1olem  24363  ovoliunlem1  25494  cxpcn3  26737  nosupbnd2  27705  noinfbnd2  27720  noseqrdglem  28322  axlowdimlem15  29050  axlowdim  29055  nvi  30710  nvop  30772  phop  30914  br8d  32707  fgreu  32770  1stpreimas  32805  rlocval  33347  rloccring  33358  smatfval  33986  smatrcl  33987  smatlem  33988  fmla0xp  35618  mvhfval  35768  mpst123  35775  br8  35991  fvtransport  36267  cbvoprab1vw  36472  cbvoprab2vw  36473  cbvoprab1davw  36506  cbvoprab2davw  36507  cbvoprab12davw  36510  bj-inftyexpitaudisj  37572  rfovcnvf1od  44455  oppcup3lem  49703  tposcurf2val  49798  oppcthinendcALT  49938  concom  50160