Theorem opeq2d 4824

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

Syntax hints:   → wi 4   = wceq 1540  ⟨cop 4579

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580

This theorem is referenced by:  dfid2  5520  funopsn  7076  fmptsng  7096  fmptsnd  7097  fvproj  8042  tfrlem11  8289  seqomlem0  8350  seqomlem1  8351  seqomlem4  8354  seqomeq12  8355  fundmen  8896  dif1en  9025  dif1enOLD  9027  unxpdomlem1  9115  mulcanenq  10817  elreal2  10989  om2uzrdg  13777  uzrdgsuci  13781  seqeq2  13826  seqeq3  13827  s1val  14402  s1eq  14404  swrdlsw  14478  pfxpfx  14519  swrdccat  14546  swrdccat3blem  14550  swrdccat3b  14551  pfxccatin12d  14556  swrds2  14752  swrds2m  14753  swrd2lsw  14764  eucalgval  16384  setsidvald  16997  setsidvaldOLD  16998  ressval  17041  ressress  17055  prdsval  17263  imasval  17319  imasaddvallem  17337  xpsfval  17374  xpsval  17378  cidval  17483  iscatd2  17487  oppcval  17519  ismon  17542  rescval  17636  idfucl  17693  funcres  17708  fucval  17772  fucpropd  17792  setcval  17889  catcval  17912  estrcval  17937  xpcval  17991  1stfcl  18011  2ndfcl  18012  curf12  18042  curf2val  18045  curfcl  18047  hofcl  18074  oduval  18103  ipoval  18345  frmdval  18586  efmnd  18605  oppgval  19047  symgvalstruct  19100  symgvalstructOLD  19101  efgmval  19413  efgmnvl  19415  efgi  19420  frgpup3lem  19478  dprd2da  19740  dmdprdpr  19747  dprdpr  19748  pgpfaclem1  19779  mgpval  19818  mgpress  19830  mgpressOLD  19831  opprval  19958  sraval  20544  rlmval2  20570  zlmval  20823  znval  20845  znval2  20847  thlval  21006  islindf4  21151  psrval  21224  opsrval  21353  opsrval2  21355  matval  21664  mat1dimmul  21731  mat1dimcrng  21732  mat1scmat  21794  mdet0pr  21847  m1detdiag  21852  txkgen  22909  pt1hmeo  23063  xpstopnlem1  23066  xpstopnlem2  23068  tusval  23523  tmsval  23742  tngval  23901  om1val  24299  pi1xfrcnvlem  24325  pi1xfrcnv  24326  dchrval  26488  nosupbnd2lem1  26969  noinfbnd2lem1  26984  ttgval  27525  ttgvalOLD  27526  eengv  27636  uspgr1ewop  27904  usgr2v1e2w  27908  1loopgruspgr  28156  1egrvtxdg1r  28166  1egrvtxdg0  28167  eupth2lem3lem3  28882  eupth2  28891  wlkl0  29019  br8d  31237  resvval  31822  idlsrgval  31945  smatfval  32043  smatrcl  32044  smatlem  32045  qqhval  32222  bnj66  33139  bnj1234  33292  bnj1296  33300  bnj1450  33329  bnj1463  33334  bnj1501  33346  bnj1523  33350  subfacp1lem5  33445  cvmliftlem10  33555  cvmlift2lem12  33575  goaleq12d  33612  sategoelfvb  33680  msubffval  33784  msubfval  33785  elmsubrn  33789  msubrn  33790  msubco  33792  br8  34012  br6  34013  btwnouttr2  34420  brfs  34477  btwnconn1lem11  34495  bj-dfid2ALT  35349  bj-endval  35599  csbfinxpg  35672  finixpnum  35875  ldualset  37400  tgrpfset  39020  tgrpset  39021  erngfset  39075  erngset  39076  erngfset-rN  39083  erngset-rN  39084  dvafset  39280  dvaset  39281  dvhfset  39356  dvhset  39357  dvhfvadd  39367  dvhopvadd2  39370  dib1dim2  39444  dicvscacl  39467  cdlemn6  39478  dihopelvalcpre  39524  dih1dimatlem  39605  hdmapfval  40103  hlhilset  40210  mendval  41279  mnringvald  42156  ovolval4lem1  44533  ovolval4lem2  44534  ovnovollem3  44542  idfusubc0  45783  idfusubc  45784  rngcvalALTV  45879  ringcvalALTV  45925  zlmodzxzsub  46056  lmod1zr  46194  2arymaptf  46358  prstcval  46705  mndtcval  46726