Theorem opeq2d 4840

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  dfid2  5548  funopsn  7149  funopsnOLD  7150  fmptsng  7171  fmptsnd  7172  fvproj  8144  tfrlem11  8389  seqomlem0  8452  seqomlem1  8453  seqomlem4  8456  seqomeq12  8457  fundmen  9052  dif1en  9170  unxpdomlem1  9240  mulcanenq  11038  elreal2  11210  om2uzrdg  14092  uzrdgsuci  14096  seqeq2  14141  seqeq3  14142  s1val  14738  s1eq  14740  swrdlsw  14810  pfxpfx  14850  swrdccat  14877  swrdccat3blem  14881  swrdccat3b  14882  pfxccatin12d  14887  swrds2  15084  swrds2m  15085  swrd2lsw  15098  eucalgval  16750  setsidvald  17370  ressval  17404  ressress  17418  prdsval  17619  imasval  17676  imasaddvallem  17694  xpsfval  17731  xpsval  17735  cidval  17844  iscatd2  17848  oppcval  17880  ismon  17901  rescval  17995  idfucl  18049  funcres  18064  idfusubc0  18067  idfusubc  18068  fucval  18129  fucpropd  18148  setcval  18245  catcval  18268  estrcval  18291  xpcval  18344  1stfcl  18364  2ndfcl  18365  curf12  18394  curf2val  18397  curfcl  18399  hofcl  18426  oduval  18455  ipoval  18697  frmdval  19040  efmnd  19059  oppgval  19554  symgvalstruct  19604  efgmval  19919  efgmnvl  19921  efgi  19926  frgpup3lem  19984  dprd2da  20251  dmdprdpr  20258  dprdpr  20259  pgpfaclem1  20290  mgpval  20356  mgpress  20363  opprval  20561  sraval  21443  rlmval2  21460  pzriprnglem10  21789  zlmval  21814  znval  21834  znval2  21836  thlval  21994  islindf4  22137  psrval  22216  opsrval  22348  opsrval2  22350  matval  22719  mat1dimmul  22784  mat1dimcrng  22785  mat1scmat  22847  mdet0pr  22900  m1detdiag  22905  txkgen  23964  pt1hmeo  24118  xpstopnlem1  24121  xpstopnlem2  24123  tusval  24577  tmsval  24793  tngval  24951  om1val  25344  pi1xfrcnvlem  25370  pi1xfrcnv  25371  dchrval  27554  nosupbnd2lem1  28065  noinfbnd2lem1  28080  seqseq123d  28665  om2noseqrdg  28683  noseqrdgsuc  28687  angmgmval  29387  ttgval  29445  eengv  29550  uspgr1ewop  29822  usgr2v1e2w  29826  1loopgruspgr  30074  1egrvtxdg1r  30084  1egrvtxdg0  30085  eupth2lem3lem3  30824  eupth2  30833  wlkl0  30961  br8d  33195  fresunsn  33212  elrgspnlem2  33797  rlocval  33813  rlocf1  33828  resvval  33883  opprabs  33999  idlsrgval  34028  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem3  34147  selvply1rhmlem5  34149  selvply1rhm  34150  mplidom  34153  extvfvcl  34161  resssra  34212  smatfval  34420  smatrcl  34421  smatlem  34422  qqhval  34597  bnj66  35483  bnj1234  35636  bnj1296  35644  bnj1450  35673  bnj1463  35678  bnj1501  35690  bnj1523  35694  subfacp1lem5  35928  cvmliftlem10  36038  cvmlift2lem12  36058  goaleq12d  36095  sategoelfvb  36163  msubffval  36267  msubfval  36268  elmsubrn  36272  msubrn  36273  msubco  36275  br8  36500  br6  36501  btwnouttr2  36767  brfs  36824  btwnconn1lem11  36842  cbvoprab3davw  37042  bj-dfid2ALT  37960  bj-endval  38216  csbfinxpg  38291  finixpnum  38508  ldualset  40162  tgrpfset  41781  tgrpset  41782  erngfset  41836  erngset  41837  erngfset-rN  41844  erngset-rN  41845  dvafset  42041  dvaset  42042  dvhfset  42117  dvhset  42118  dvhfvadd  42128  dvhopvadd2  42131  dib1dim2  42205  dicvscacl  42228  cdlemn6  42239  dihopelvalcpre  42285  dih1dimatlem  42366  hdmapfval  42864  hlhilset  42971  mendval  44165  mnringvald  45196  ovolval4lem1  47628  ovolval4lem2  47629  ovnovollem3  47637  isubgrvtxuhgr  48931  isubgr0uhgr  48940  stgrfv  49020  gpgov  49109  gpgprismgriedgdmss  49119  gpgvtx0  49120  gpgvtx1  49121  gpgedgvtx0  49128  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedgiov  49132  gpgedg2ov  49133  gpgedg2iv  49134  gpg3kgrtriexlem6  49155  gpg3kgrtriex  49156  gpgprismgr4cycllem3  49164  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5  49190  gpg5edgnedg  49197  rngcvalALTV  49331  ringcvalALTV  49355  zlmodzxzsub  49441  lmod1zr  49574  2arymaptf  49733  discsubc  50141  2oppf  50209  upfval2  50254  upfval3  50255  isuplem  50256  uptpos  50275  uptr2  50298  dfswapf2  50338  oppc1stf  50365  oppc2ndf  50366  fucolid  50438  fucorid  50439  precofval2  50446  prcofval  50455  isinito2lem  50575  termcfuncval  50609  prstcval  50628  mndtcval  50656  lanup  50718  coccom  50741  iscmd  50743