Theorem opeq2d 4847

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599

This theorem is referenced by:  dfid2  5538  funopsn  7123  fmptsng  7145  fmptsnd  7146  fvproj  8116  tfrlem11  8359  seqomlem0  8420  seqomlem1  8421  seqomlem4  8424  seqomeq12  8425  fundmen  9005  dif1en  9130  dif1enOLD  9132  unxpdomlem1  9204  mulcanenq  10920  elreal2  11092  om2uzrdg  13928  uzrdgsuci  13932  seqeq2  13977  seqeq3  13978  s1val  14570  s1eq  14572  swrdlsw  14639  pfxpfx  14680  swrdccat  14707  swrdccat3blem  14711  swrdccat3b  14712  pfxccatin12d  14717  swrds2  14913  swrds2m  14914  swrd2lsw  14925  eucalgval  16559  setsidvald  17176  ressval  17210  ressress  17224  prdsval  17425  imasval  17481  imasaddvallem  17499  xpsfval  17536  xpsval  17540  cidval  17645  iscatd2  17649  oppcval  17681  ismon  17702  rescval  17796  idfucl  17850  funcres  17865  idfusubc0  17868  idfusubc  17869  fucval  17930  fucpropd  17949  setcval  18046  catcval  18069  estrcval  18092  xpcval  18145  1stfcl  18165  2ndfcl  18166  curf12  18195  curf2val  18198  curfcl  18200  hofcl  18227  oduval  18256  ipoval  18496  frmdval  18785  efmnd  18804  oppgval  19286  symgvalstruct  19334  efgmval  19649  efgmnvl  19651  efgi  19656  frgpup3lem  19714  dprd2da  19981  dmdprdpr  19988  dprdpr  19989  pgpfaclem1  20020  mgpval  20059  mgpress  20066  opprval  20254  sraval  21089  rlmval2  21106  pzriprnglem10  21407  zlmval  21432  znval  21452  znval2  21454  thlval  21611  islindf4  21754  psrval  21831  opsrval  21960  opsrval2  21962  matval  22305  mat1dimmul  22370  mat1dimcrng  22371  mat1scmat  22433  mdet0pr  22486  m1detdiag  22491  txkgen  23546  pt1hmeo  23700  xpstopnlem1  23703  xpstopnlem2  23705  tusval  24160  tmsval  24376  tngval  24534  om1val  24937  pi1xfrcnvlem  24963  pi1xfrcnv  24964  dchrval  27152  nosupbnd2lem1  27634  noinfbnd2lem1  27649  seqseq123d  28187  om2noseqrdg  28205  noseqrdgsuc  28209  ttgval  28809  eengv  28913  uspgr1ewop  29182  usgr2v1e2w  29186  1loopgruspgr  29435  1egrvtxdg1r  29445  1egrvtxdg0  29446  eupth2lem3lem3  30166  eupth2  30175  wlkl0  30303  br8d  32545  elrgspnlem2  33201  rlocval  33217  rlocf1  33231  resvval  33308  opprabs  33460  idlsrgval  33481  resssra  33590  smatfval  33792  smatrcl  33793  smatlem  33794  qqhval  33969  bnj66  34857  bnj1234  35010  bnj1296  35018  bnj1450  35047  bnj1463  35052  bnj1501  35064  bnj1523  35068  subfacp1lem5  35178  cvmliftlem10  35288  cvmlift2lem12  35308  goaleq12d  35345  sategoelfvb  35413  msubffval  35517  msubfval  35518  elmsubrn  35522  msubrn  35523  msubco  35525  br8  35750  br6  35751  btwnouttr2  36017  brfs  36074  btwnconn1lem11  36092  cbvoprab3davw  36268  bj-dfid2ALT  37060  bj-endval  37310  csbfinxpg  37383  finixpnum  37606  ldualset  39125  tgrpfset  40745  tgrpset  40746  erngfset  40800  erngset  40801  erngfset-rN  40808  erngset-rN  40809  dvafset  41005  dvaset  41006  dvhfset  41081  dvhset  41082  dvhfvadd  41092  dvhopvadd2  41095  dib1dim2  41169  dicvscacl  41192  cdlemn6  41203  dihopelvalcpre  41249  dih1dimatlem  41330  hdmapfval  41828  hlhilset  41935  mendval  43175  mnringvald  44209  ovolval4lem1  46654  ovolval4lem2  46655  ovnovollem3  46663  isubgrvtxuhgr  47868  isubgr0uhgr  47877  stgrfv  47956  gpgov  48037  gpgprismgriedgdmss  48047  gpgvtx0  48048  gpgvtx1  48049  gpgedgvtx0  48056  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2ov  48061  gpgedg2iv  48062  gpg3kgrtriexlem6  48083  gpg3kgrtriex  48084  gpgprismgr4cycllem3  48091  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  rngcvalALTV  48257  ringcvalALTV  48281  zlmodzxzsub  48352  lmod1zr  48486  2arymaptf  48645  discsubc  49057  2oppf  49125  upfval2  49170  upfval3  49171  isuplem  49172  uptpos  49191  uptr2  49214  dfswapf2  49254  oppc1stf  49281  oppc2ndf  49282  fucolid  49354  fucorid  49355  precofval2  49362  prcofval  49371  isinito2lem  49491  termcfuncval  49525  prstcval  49544  mndtcval  49572  lanup  49634  coccom  49657  iscmd  49659