Theorem opeq2d 4808

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

Syntax hints:   → wi 4   = wceq 1539  ⟨cop 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565

This theorem is referenced by:  dfid2  5482  funopsn  7002  fmptsng  7022  fmptsnd  7023  fvproj  7946  tfrlem11  8190  seqomlem0  8250  seqomlem1  8251  seqomlem4  8254  seqomeq12  8255  fundmen  8775  dif1en  8907  unxpdomlem1  8956  mulcanenq  10647  elreal2  10819  om2uzrdg  13604  uzrdgsuci  13608  seqeq2  13653  seqeq3  13654  s1val  14231  s1eq  14233  swrdlsw  14308  pfxpfx  14349  swrdccat  14376  swrdccat3blem  14380  swrdccat3b  14381  pfxccatin12d  14386  swrds2  14581  swrds2m  14582  swrd2lsw  14593  eucalgval  16215  setsidvald  16828  setsidvaldOLD  16829  ressval  16870  ressress  16884  prdsval  17083  imasval  17139  imasaddvallem  17157  xpsfval  17194  xpsval  17198  cidval  17303  iscatd2  17307  oppcval  17339  ismon  17362  rescval  17456  idfucl  17512  funcres  17527  fucval  17591  fucpropd  17611  setcval  17708  catcval  17731  estrcval  17756  xpcval  17810  1stfcl  17830  2ndfcl  17831  curf12  17861  curf2val  17864  curfcl  17866  hofcl  17893  oduval  17922  ipoval  18163  frmdval  18405  efmnd  18424  oppgval  18866  symgvalstruct  18919  symgvalstructOLD  18920  efgmval  19233  efgmnvl  19235  efgi  19240  frgpup3lem  19298  dprd2da  19560  dmdprdpr  19567  dprdpr  19568  pgpfaclem1  19599  mgpval  19638  mgpress  19650  mgpressOLD  19651  opprval  19778  sraval  20353  rlmval2  20377  zlmval  20629  znval  20651  znval2  20653  thlval  20812  islindf4  20955  psrval  21028  opsrval  21157  opsrval2  21159  matval  21468  mat1dimmul  21533  mat1dimcrng  21534  mat1scmat  21596  mdet0pr  21649  m1detdiag  21654  txkgen  22711  pt1hmeo  22865  xpstopnlem1  22868  xpstopnlem2  22870  tusval  23325  tmsval  23542  tngval  23701  om1val  24099  pi1xfrcnvlem  24125  pi1xfrcnv  24126  dchrval  26287  ttgval  27140  eengv  27250  uspgr1ewop  27518  usgr2v1e2w  27522  1loopgruspgr  27770  1egrvtxdg1r  27780  1egrvtxdg0  27781  eupth2lem3lem3  28495  eupth2  28504  wlkl0  28632  br8d  30851  resvval  31428  idlsrgval  31550  smatfval  31647  smatrcl  31648  smatlem  31649  qqhval  31824  bnj66  32740  bnj1234  32893  bnj1296  32901  bnj1450  32930  bnj1463  32935  bnj1501  32947  bnj1523  32951  subfacp1lem5  33046  cvmliftlem10  33156  cvmlift2lem12  33176  goaleq12d  33213  sategoelfvb  33281  msubffval  33385  msubfval  33386  elmsubrn  33390  msubrn  33391  msubco  33393  br8  33629  br6  33630  nosupbnd2lem1  33845  noinfbnd2lem1  33860  btwnouttr2  34251  brfs  34308  btwnconn1lem11  34326  bj-dfid2ALT  35163  bj-endval  35413  csbfinxpg  35486  finixpnum  35689  ldualset  37066  tgrpfset  38685  tgrpset  38686  erngfset  38740  erngset  38741  erngfset-rN  38748  erngset-rN  38749  dvafset  38945  dvaset  38946  dvhfset  39021  dvhset  39022  dvhfvadd  39032  dvhopvadd2  39035  dib1dim2  39109  dicvscacl  39132  cdlemn6  39143  dihopelvalcpre  39189  dih1dimatlem  39270  hdmapfval  39768  hlhilset  39875  mendval  40924  mnringvald  41715  ovolval4lem1  44077  ovolval4lem2  44078  ovnovollem3  44086  idfusubc0  45311  idfusubc  45312  rngcvalALTV  45407  ringcvalALTV  45453  zlmodzxzsub  45584  lmod1zr  45722  2arymaptf  45886  prstcval  46233  mndtcval  46252