Theorem opeq2d 4884

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

Syntax hints:   → wi 4   = wceq 1536  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  dfid2  5584  funopsn  7167  fmptsng  7187  fmptsnd  7188  fvproj  8157  tfrlem11  8426  seqomlem0  8487  seqomlem1  8488  seqomlem4  8491  seqomeq12  8492  fundmen  9069  dif1en  9198  dif1enOLD  9200  unxpdomlem1  9283  mulcanenq  10997  elreal2  11169  om2uzrdg  13993  uzrdgsuci  13997  seqeq2  14042  seqeq3  14043  s1val  14632  s1eq  14634  swrdlsw  14701  pfxpfx  14742  swrdccat  14769  swrdccat3blem  14773  swrdccat3b  14774  pfxccatin12d  14779  swrds2  14975  swrds2m  14976  swrd2lsw  14987  eucalgval  16615  setsidvald  17232  setsidvaldOLD  17233  ressval  17276  ressress  17293  prdsval  17501  imasval  17557  imasaddvallem  17575  xpsfval  17612  xpsval  17616  cidval  17721  iscatd2  17725  oppcval  17757  ismon  17780  rescval  17874  idfucl  17931  funcres  17946  idfusubc0  17949  idfusubc  17950  fucval  18013  fucpropd  18033  setcval  18130  catcval  18153  estrcval  18178  xpcval  18232  1stfcl  18252  2ndfcl  18253  curf12  18283  curf2val  18286  curfcl  18288  hofcl  18315  oduval  18344  ipoval  18587  frmdval  18876  efmnd  18895  oppgval  19377  symgvalstruct  19428  symgvalstructOLD  19429  efgmval  19744  efgmnvl  19746  efgi  19751  frgpup3lem  19809  dprd2da  20076  dmdprdpr  20083  dprdpr  20084  pgpfaclem1  20115  mgpval  20154  mgpress  20166  mgpressOLD  20167  opprval  20351  sraval  21191  rlmval2  21216  pzriprnglem10  21518  zlmval  21543  znval  21567  znval2  21569  thlval  21730  islindf4  21875  psrval  21952  opsrval  22081  opsrval2  22083  matval  22430  mat1dimmul  22497  mat1dimcrng  22498  mat1scmat  22560  mdet0pr  22613  m1detdiag  22618  txkgen  23675  pt1hmeo  23829  xpstopnlem1  23832  xpstopnlem2  23834  tusval  24289  tmsval  24508  tngval  24667  om1val  25076  pi1xfrcnvlem  25102  pi1xfrcnv  25103  dchrval  27292  nosupbnd2lem1  27774  noinfbnd2lem1  27789  seqseq123d  28306  om2noseqrdg  28324  noseqrdgsuc  28328  ttgval  28897  ttgvalOLD  28898  eengv  29008  uspgr1ewop  29279  usgr2v1e2w  29283  1loopgruspgr  29532  1egrvtxdg1r  29542  1egrvtxdg0  29543  eupth2lem3lem3  30258  eupth2  30267  wlkl0  30395  br8d  32629  elrgspnlem2  33232  rlocval  33245  rlocf1  33259  resvval  33332  opprabs  33489  idlsrgval  33510  resssra  33616  smatfval  33755  smatrcl  33756  smatlem  33757  qqhval  33934  bnj66  34852  bnj1234  35005  bnj1296  35013  bnj1450  35042  bnj1463  35047  bnj1501  35059  bnj1523  35063  subfacp1lem5  35168  cvmliftlem10  35278  cvmlift2lem12  35298  goaleq12d  35335  sategoelfvb  35403  msubffval  35507  msubfval  35508  elmsubrn  35512  msubrn  35513  msubco  35515  br8  35735  br6  35736  btwnouttr2  36003  brfs  36060  btwnconn1lem11  36078  cbvoprab3davw  36255  bj-dfid2ALT  37047  bj-endval  37297  csbfinxpg  37370  finixpnum  37591  ldualset  39106  tgrpfset  40726  tgrpset  40727  erngfset  40781  erngset  40782  erngfset-rN  40789  erngset-rN  40790  dvafset  40986  dvaset  40987  dvhfset  41062  dvhset  41063  dvhfvadd  41073  dvhopvadd2  41076  dib1dim2  41150  dicvscacl  41173  cdlemn6  41184  dihopelvalcpre  41230  dih1dimatlem  41311  hdmapfval  41809  hlhilset  41916  mendval  43167  mnringvald  44203  ovolval4lem1  46604  ovolval4lem2  46605  ovnovollem3  46613  isubgrvtxuhgr  47787  isubgr0uhgr  47796  stgrfv  47855  gpgov  47936  gpgvtx0  47943  gpgvtx1  47944  gpgedgvtx0  47953  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  rngcvalALTV  48108  ringcvalALTV  48132  zlmodzxzsub  48204  lmod1zr  48338  2arymaptf  48501  prstcval  48864  mndtcval  48887