Theorem opeq2d 4856

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608

This theorem is referenced by:  dfid2  5550  funopsn  7137  fmptsng  7159  fmptsnd  7160  fvproj  8131  tfrlem11  8400  seqomlem0  8461  seqomlem1  8462  seqomlem4  8465  seqomeq12  8466  fundmen  9043  dif1en  9172  dif1enOLD  9174  unxpdomlem1  9256  mulcanenq  10972  elreal2  11144  om2uzrdg  13972  uzrdgsuci  13976  seqeq2  14021  seqeq3  14022  s1val  14614  s1eq  14616  swrdlsw  14683  pfxpfx  14724  swrdccat  14751  swrdccat3blem  14755  swrdccat3b  14756  pfxccatin12d  14761  swrds2  14957  swrds2m  14958  swrd2lsw  14969  eucalgval  16599  setsidvald  17216  ressval  17252  ressress  17266  prdsval  17467  imasval  17523  imasaddvallem  17541  xpsfval  17578  xpsval  17582  cidval  17687  iscatd2  17691  oppcval  17723  ismon  17744  rescval  17838  idfucl  17892  funcres  17907  idfusubc0  17910  idfusubc  17911  fucval  17972  fucpropd  17991  setcval  18088  catcval  18111  estrcval  18134  xpcval  18187  1stfcl  18207  2ndfcl  18208  curf12  18237  curf2val  18240  curfcl  18242  hofcl  18269  oduval  18298  ipoval  18538  frmdval  18827  efmnd  18846  oppgval  19328  symgvalstruct  19376  efgmval  19691  efgmnvl  19693  efgi  19698  frgpup3lem  19756  dprd2da  20023  dmdprdpr  20030  dprdpr  20031  pgpfaclem1  20062  mgpval  20101  mgpress  20108  opprval  20296  sraval  21131  rlmval2  21148  pzriprnglem10  21449  zlmval  21474  znval  21494  znval2  21496  thlval  21653  islindf4  21796  psrval  21873  opsrval  22002  opsrval2  22004  matval  22347  mat1dimmul  22412  mat1dimcrng  22413  mat1scmat  22475  mdet0pr  22528  m1detdiag  22533  txkgen  23588  pt1hmeo  23742  xpstopnlem1  23745  xpstopnlem2  23747  tusval  24202  tmsval  24418  tngval  24576  om1val  24979  pi1xfrcnvlem  25005  pi1xfrcnv  25006  dchrval  27195  nosupbnd2lem1  27677  noinfbnd2lem1  27692  seqseq123d  28209  om2noseqrdg  28227  noseqrdgsuc  28231  ttgval  28800  eengv  28904  uspgr1ewop  29173  usgr2v1e2w  29177  1loopgruspgr  29426  1egrvtxdg1r  29436  1egrvtxdg0  29437  eupth2lem3lem3  30157  eupth2  30166  wlkl0  30294  br8d  32536  elrgspnlem2  33184  rlocval  33200  rlocf1  33214  resvval  33291  opprabs  33443  idlsrgval  33464  resssra  33573  smatfval  33772  smatrcl  33773  smatlem  33774  qqhval  33949  bnj66  34837  bnj1234  34990  bnj1296  34998  bnj1450  35027  bnj1463  35032  bnj1501  35044  bnj1523  35048  subfacp1lem5  35152  cvmliftlem10  35262  cvmlift2lem12  35282  goaleq12d  35319  sategoelfvb  35387  msubffval  35491  msubfval  35492  elmsubrn  35496  msubrn  35497  msubco  35499  br8  35719  br6  35720  btwnouttr2  35986  brfs  36043  btwnconn1lem11  36061  cbvoprab3davw  36237  bj-dfid2ALT  37029  bj-endval  37279  csbfinxpg  37352  finixpnum  37575  ldualset  39089  tgrpfset  40709  tgrpset  40710  erngfset  40764  erngset  40765  erngfset-rN  40772  erngset-rN  40773  dvafset  40969  dvaset  40970  dvhfset  41045  dvhset  41046  dvhfvadd  41056  dvhopvadd2  41059  dib1dim2  41133  dicvscacl  41156  cdlemn6  41167  dihopelvalcpre  41213  dih1dimatlem  41294  hdmapfval  41792  hlhilset  41899  mendval  43150  mnringvald  44185  ovolval4lem1  46626  ovolval4lem2  46627  ovnovollem3  46635  isubgrvtxuhgr  47825  isubgr0uhgr  47834  stgrfv  47913  gpgov  47994  gpgprismgriedgdmss  48004  gpgvtx0  48005  gpgvtx1  48006  gpgedgvtx0  48013  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg3kgrtriexlem6  48038  gpg3kgrtriex  48039  gpgprismgr4cycllem3  48044  rngcvalALTV  48188  ringcvalALTV  48212  zlmodzxzsub  48283  lmod1zr  48417  2arymaptf  48580  discsubc  48979  2oppf  49028  upfval2  49060  upfval3  49061  isuplem  49062  uptpos  49079  dfswapf2  49126  fucolid  49220  fucorid  49221  precofval2  49228  prcofval  49237  isinito2lem  49331  termcfuncval  49365  prstcval  49376  mndtcval  49404  lanup  49463  coccom  49482  iscmd  49484