Theorem opeq2d 4852

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ⟨cop 4840

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  dfid2  5555  funopsn  7183  funopsnOLD  7184  fmptsng  7204  fmptsnd  7205  fvproj  8188  tfrlem11  8434  seqomlem0  8497  seqomlem1  8498  seqomlem4  8501  seqomeq12  8502  fundmen  9097  dif1en  9215  unxpdomlem1  9285  mulcanenq  11084  elreal2  11256  om2uzrdg  14139  uzrdgsuci  14143  seqeq2  14188  seqeq3  14189  s1val  14786  s1eq  14788  swrdlsw  14859  pfxpfx  14899  swrdccat  14926  swrdccat3blem  14930  swrdccat3b  14931  pfxccatin12d  14936  swrds2  15134  swrds2m  15135  swrd2lsw  15148  eucalgval  16801  setsidvald  17421  ressval  17455  ressress  17469  prdsval  17676  imasval  17733  imasaddvallem  17751  xpsfval  17788  xpsval  17792  cidval  17901  iscatd2  17905  oppcval  17937  ismon  17958  rescval  18052  idfucl  18106  funcres  18121  idfusubc0  18124  idfusubc  18125  fucval  18186  fucpropd  18205  setcval  18302  catcval  18325  estrcval  18348  xpcval  18401  1stfcl  18421  2ndfcl  18422  curf12  18451  curf2val  18454  curfcl  18456  hofcl  18483  oduval  18512  ipoval  18754  frmdval  19097  efmnd  19116  oppgval  19612  symgvalstruct  19662  efgmval  19977  efgmnvl  19979  efgi  19984  frgpup3lem  20042  dprd2da  20309  dmdprdpr  20316  dprdpr  20317  pgpfaclem1  20348  mgpval  20414  mgpress  20421  opprval  20619  sraval  21501  rlmval2  21518  pzriprnglem10  21851  zlmval  21876  znval  21896  znval2  21898  thlval  22056  islindf4  22199  psrval  22278  opsrval  22410  opsrval2  22412  matval  22781  mat1dimmul  22846  mat1dimcrng  22847  mat1scmat  22909  mdet0pr  22962  m1detdiag  22967  txkgen  24026  pt1hmeo  24180  xpstopnlem1  24183  xpstopnlem2  24185  tusval  24639  tmsval  24855  tngval  25013  om1val  25406  pi1xfrcnvlem  25432  pi1xfrcnv  25433  dchrval  27618  nosupbnd2lem1  28129  noinfbnd2lem1  28144  seqseq123d  28729  om2noseqrdg  28747  noseqrdgsuc  28751  angmgmval  29451  ttgval  29509  eengv  29614  uspgr1ewop  29886  usgr2v1e2w  29890  1loopgruspgr  30138  1egrvtxdg1r  30148  1egrvtxdg0  30149  eupth2lem3lem3  30888  eupth2  30897  wlkl0  31025  br8d  33300  fresunsn  33317  elrgspnlem2  33903  rlocval  33919  rlocf1  33934  resvval  33994  opprabs  34110  idlsrgval  34139  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem3  34265  selvply1rhmlem5  34267  selvply1rhm  34268  mplidom  34271  extvfvcl  34279  resssra  34330  smatfval  34538  smatrcl  34539  smatlem  34540  qqhval  34715  bnj66  35601  bnj1234  35754  bnj1296  35762  bnj1450  35791  bnj1463  35796  bnj1501  35808  bnj1523  35812  subfacp1lem5  36157  cvmliftlem10  36267  cvmlift2lem12  36287  goaleq12d  36324  sategoelfvb  36392  msubffval  36496  msubfval  36497  elmsubrn  36501  msubrn  36502  msubco  36504  br8  36736  br6  36737  btwnouttr2  37002  brfs  37059  btwnconn1lem11  37077  cbvoprab3davw  37277  bj-dfid2ALT  38250  bj-endval  38504  csbfinxpg  38579  finixpnum  38796  ldualset  40448  tgrpfset  42067  tgrpset  42068  erngfset  42122  erngset  42123  erngfset-rN  42130  erngset-rN  42131  dvafset  42327  dvaset  42328  dvhfset  42403  dvhset  42404  dvhfvadd  42414  dvhopvadd2  42417  dib1dim2  42491  dicvscacl  42514  cdlemn6  42525  dihopelvalcpre  42571  dih1dimatlem  42652  hdmapfval  43150  hlhilset  43257  mendval  44442  mnringvald  45472  ovolval4lem1  47932  ovolval4lem2  47933  ovnovollem3  47941  isubgrvtxuhgr  49235  isubgr0uhgr  49244  stgrfv  49324  gpgov  49413  gpgprismgriedgdmss  49423  gpgvtx0  49424  gpgvtx1  49425  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedgiov  49436  gpgedg2ov  49437  gpgedg2iv  49438  gpg3kgrtriexlem6  49459  gpg3kgrtriex  49460  gpgprismgr4cycllem3  49468  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5  49494  gpg5edgnedg  49501  rngcvalALTV  49635  ringcvalALTV  49659  zlmodzxzsub  49803  lmod1zr  49936  2arymaptf  50095  discsubc  50509  2oppf  50579  upfval2  50624  upfval3  50625  isuplem  50626  uptpos  50645  uptr2  50668  dfswapf2  50714  oppc1stf  50741  oppc2ndf  50742  fucolid  50814  fucorid  50815  precofval2  50835  prcofval  50844  isinito2lem  50964  termcfuncval  50998  termcfunc1eq  51001  prstcval  51020  mndtcval  51048  lanup  51155  coccom  51178  iscmd  51180