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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  dfid2  5528  funopsn  7102  fmptsng  7124  fmptsnd  7125  fvproj  8090  tfrlem11  8333  seqomlem0  8394  seqomlem1  8395  seqomlem4  8398  seqomeq12  8399  fundmen  8979  dif1en  9101  dif1enOLD  9103  unxpdomlem1  9173  mulcanenq  10889  elreal2  11061  om2uzrdg  13897  uzrdgsuci  13901  seqeq2  13946  seqeq3  13947  s1val  14539  s1eq  14541  swrdlsw  14608  pfxpfx  14649  swrdccat  14676  swrdccat3blem  14680  swrdccat3b  14681  pfxccatin12d  14686  swrds2  14882  swrds2m  14883  swrd2lsw  14894  eucalgval  16528  setsidvald  17145  ressval  17179  ressress  17193  prdsval  17394  imasval  17450  imasaddvallem  17468  xpsfval  17505  xpsval  17509  cidval  17614  iscatd2  17618  oppcval  17650  ismon  17671  rescval  17765  idfucl  17819  funcres  17834  idfusubc0  17837  idfusubc  17838  fucval  17899  fucpropd  17918  setcval  18015  catcval  18038  estrcval  18061  xpcval  18114  1stfcl  18134  2ndfcl  18135  curf12  18164  curf2val  18167  curfcl  18169  hofcl  18196  oduval  18225  ipoval  18465  frmdval  18754  efmnd  18773  oppgval  19255  symgvalstruct  19303  efgmval  19618  efgmnvl  19620  efgi  19625  frgpup3lem  19683  dprd2da  19950  dmdprdpr  19957  dprdpr  19958  pgpfaclem1  19989  mgpval  20028  mgpress  20035  opprval  20223  sraval  21058  rlmval2  21075  pzriprnglem10  21376  zlmval  21401  znval  21421  znval2  21423  thlval  21580  islindf4  21723  psrval  21800  opsrval  21929  opsrval2  21931  matval  22274  mat1dimmul  22339  mat1dimcrng  22340  mat1scmat  22402  mdet0pr  22455  m1detdiag  22460  txkgen  23515  pt1hmeo  23669  xpstopnlem1  23672  xpstopnlem2  23674  tusval  24129  tmsval  24345  tngval  24503  om1val  24906  pi1xfrcnvlem  24932  pi1xfrcnv  24933  dchrval  27121  nosupbnd2lem1  27603  noinfbnd2lem1  27618  seqseq123d  28156  om2noseqrdg  28174  noseqrdgsuc  28178  ttgval  28778  eengv  28882  uspgr1ewop  29151  usgr2v1e2w  29155  1loopgruspgr  29404  1egrvtxdg1r  29414  1egrvtxdg0  29415  eupth2lem3lem3  30132  eupth2  30141  wlkl0  30269  br8d  32511  elrgspnlem2  33167  rlocval  33183  rlocf1  33197  resvval  33274  opprabs  33426  idlsrgval  33447  resssra  33556  smatfval  33758  smatrcl  33759  smatlem  33760  qqhval  33935  bnj66  34823  bnj1234  34976  bnj1296  34984  bnj1450  35013  bnj1463  35018  bnj1501  35030  bnj1523  35034  subfacp1lem5  35144  cvmliftlem10  35254  cvmlift2lem12  35274  goaleq12d  35311  sategoelfvb  35379  msubffval  35483  msubfval  35484  elmsubrn  35488  msubrn  35489  msubco  35491  br8  35716  br6  35717  btwnouttr2  35983  brfs  36040  btwnconn1lem11  36058  cbvoprab3davw  36234  bj-dfid2ALT  37026  bj-endval  37276  csbfinxpg  37349  finixpnum  37572  ldualset  39091  tgrpfset  40711  tgrpset  40712  erngfset  40766  erngset  40767  erngfset-rN  40774  erngset-rN  40775  dvafset  40971  dvaset  40972  dvhfset  41047  dvhset  41048  dvhfvadd  41058  dvhopvadd2  41061  dib1dim2  41135  dicvscacl  41158  cdlemn6  41169  dihopelvalcpre  41215  dih1dimatlem  41296  hdmapfval  41794  hlhilset  41901  mendval  43141  mnringvald  44175  ovolval4lem1  46620  ovolval4lem2  46621  ovnovollem3  46629  isubgrvtxuhgr  47837  isubgr0uhgr  47846  stgrfv  47925  gpgov  48006  gpgprismgriedgdmss  48016  gpgvtx0  48017  gpgvtx1  48018  gpgedgvtx0  48025  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedgiov  48029  gpgedg2ov  48030  gpgedg2iv  48031  gpg3kgrtriexlem6  48052  gpg3kgrtriex  48053  gpgprismgr4cycllem3  48060  pgnbgreunbgrlem1  48076  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5  48086  rngcvalALTV  48226  ringcvalALTV  48250  zlmodzxzsub  48321  lmod1zr  48455  2arymaptf  48614  discsubc  49026  2oppf  49094  upfval2  49139  upfval3  49140  isuplem  49141  uptpos  49160  uptr2  49183  dfswapf2  49223  oppc1stf  49250  oppc2ndf  49251  fucolid  49323  fucorid  49324  precofval2  49331  prcofval  49340  isinito2lem  49460  termcfuncval  49494  prstcval  49513  mndtcval  49541  lanup  49603  coccom  49626  iscmd  49628