Theorem opeq2d 4810

Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.)

Hypothesis

Ref	Expression
opeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
opeq2d	⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2d

Step	Hyp	Ref	Expression
1		opeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		opeq2 4804	. 2 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
3	1, 2	syl 17	1 ⊢ (𝜑 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   = wceq 1537  ⟨cop 4573

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  funopsn  6910  fmptsng  6930  fmptsnd  6931  fvproj  7828  tfrlem11  8024  seqomlem0  8085  seqomlem1  8086  seqomlem4  8089  seqomeq12  8090  fundmen  8583  unxpdomlem1  8722  mulcanenq  10382  elreal2  10554  om2uzrdg  13325  uzrdgsuci  13329  seqeq2  13374  seqeq3  13375  s1val  13952  s1eq  13954  swrdlsw  14029  pfxpfx  14070  swrdccat  14097  swrdccat3blem  14101  swrdccat3b  14102  pfxccatin12d  14107  swrds2  14302  swrds2m  14303  swrd2lsw  14314  eucalgval  15926  setsidvald  16514  ressval  16551  ressress  16562  prdsval  16728  imasval  16784  imasaddvallem  16802  xpsfval  16839  xpsval  16843  cidval  16948  iscatd2  16952  oppcval  16983  ismon  17003  rescval  17097  idfucl  17151  funcres  17166  fucval  17228  fucpropd  17247  setcval  17337  catcval  17356  estrcval  17374  xpcval  17427  1stfcl  17447  2ndfcl  17448  curf12  17477  curf2val  17480  curfcl  17482  hofcl  17509  oduval  17740  ipoval  17764  frmdval  18016  efmnd  18035  oppgval  18475  symgvalstruct  18525  efgmval  18838  efgmnvl  18840  efgi  18845  frgpup3lem  18903  dprd2da  19164  dmdprdpr  19171  dprdpr  19172  pgpfaclem1  19203  mgpval  19242  mgpress  19250  opprval  19374  sraval  19948  rlmval2  19966  psrval  20142  opsrval  20255  opsrval2  20257  zlmval  20663  znval  20682  znval2  20684  thlval  20839  islindf4  20982  matval  21020  mat1dimmul  21085  mat1dimcrng  21086  mat1scmat  21148  mdet0pr  21201  m1detdiag  21206  txkgen  22260  pt1hmeo  22414  xpstopnlem1  22417  xpstopnlem2  22419  tusval  22875  tmsval  23091  tngval  23248  om1val  23634  pi1xfrcnvlem  23660  pi1xfrcnv  23661  dchrval  25810  ttgval  26661  eengv  26765  uspgr1ewop  27030  usgr2v1e2w  27034  1loopgruspgr  27282  1egrvtxdg1r  27292  1egrvtxdg0  27293  eupth2lem3lem3  28009  eupth2  28018  wlkl0  28146  br8d  30361  resvval  30900  smatfval  31060  smatrcl  31061  smatlem  31062  qqhval  31215  bnj66  32132  bnj1234  32285  bnj1296  32293  bnj1450  32322  bnj1463  32327  bnj1501  32339  bnj1523  32343  subfacp1lem5  32431  cvmliftlem10  32541  cvmlift2lem12  32561  goaleq12d  32598  sategoelfvb  32666  msubffval  32770  msubfval  32771  elmsubrn  32775  msubrn  32776  msubco  32778  br8  32992  br6  32993  nosupbnd2lem1  33215  btwnouttr2  33483  brfs  33540  btwnconn1lem11  33558  bj-endval  34599  csbfinxpg  34672  finixpnum  34892  ldualset  36276  tgrpfset  37895  tgrpset  37896  erngfset  37950  erngset  37951  erngfset-rN  37958  erngset-rN  37959  dvafset  38155  dvaset  38156  dvhfset  38231  dvhset  38232  dvhfvadd  38242  dvhopvadd2  38245  dib1dim2  38319  dicvscacl  38342  cdlemn6  38353  dihopelvalcpre  38399  dih1dimatlem  38480  hdmapfval  38978  hlhilset  39085  mendval  39803  ovolval4lem1  42951  ovolval4lem2  42952  ovnovollem3  42960  idfusubc0  44156  idfusubc  44157  rngcvalALTV  44252  ringcvalALTV  44298  zlmodzxzsub  44428  lmod1zr  44568