Theorem opeq1d 3868

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

Syntax hints:   → wi 4   = wceq 1397  ⟨cop 3672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678

This theorem is referenced by:  oteq1  3871  oteq2  3872  opth  4329  cbvoprab2  6094  djuf1olem  7252  dfplpq2  7574  ltexnqq  7628  nnanq0  7678  addpinq1  7684  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prsrriota  8008  caucvgsrlemfv  8011  caucvgsr  8022  pitonnlem2  8067  pitonn  8068  recidpirq  8078  ax1rid  8097  axrnegex  8099  nntopi  8114  axcaucvglemval  8117  fseq1m1p1  10330  frecuzrdglem  10674  frecuzrdgg  10679  frecuzrdgdomlem  10680  frecuzrdgfunlem  10682  frecuzrdgsuctlem  10686  pfxswrd  11291  swrdccat  11320  swrdccat3blem  11324  fsum2dlemstep  12000  fprod2dlemstep  12188  ennnfonelemp1  13032  ennnfonelemnn0  13048  setscomd  13128  imasaddvallemg  13403