Theorem opeq2d 4836

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

Syntax hints:   → wi 4   = wceq 1541  ⟨cop 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  dfid2  5521  funopsn  7093  fmptsng  7114  fmptsnd  7115  fvproj  8076  tfrlem11  8319  seqomlem0  8380  seqomlem1  8381  seqomlem4  8384  seqomeq12  8385  fundmen  8968  dif1en  9086  unxpdomlem1  9156  mulcanenq  10871  elreal2  11043  om2uzrdg  13879  uzrdgsuci  13883  seqeq2  13928  seqeq3  13929  s1val  14522  s1eq  14524  swrdlsw  14591  pfxpfx  14631  swrdccat  14658  swrdccat3blem  14662  swrdccat3b  14663  pfxccatin12d  14668  swrds2  14863  swrds2m  14864  swrd2lsw  14875  eucalgval  16509  setsidvald  17126  ressval  17160  ressress  17174  prdsval  17375  imasval  17432  imasaddvallem  17450  xpsfval  17487  xpsval  17491  cidval  17600  iscatd2  17604  oppcval  17636  ismon  17657  rescval  17751  idfucl  17805  funcres  17820  idfusubc0  17823  idfusubc  17824  fucval  17885  fucpropd  17904  setcval  18001  catcval  18024  estrcval  18047  xpcval  18100  1stfcl  18120  2ndfcl  18121  curf12  18150  curf2val  18153  curfcl  18155  hofcl  18182  oduval  18211  ipoval  18453  frmdval  18776  efmnd  18795  oppgval  19276  symgvalstruct  19326  efgmval  19641  efgmnvl  19643  efgi  19648  frgpup3lem  19706  dprd2da  19973  dmdprdpr  19980  dprdpr  19981  pgpfaclem1  20012  mgpval  20078  mgpress  20085  opprval  20274  sraval  21127  rlmval2  21144  pzriprnglem10  21445  zlmval  21470  znval  21490  znval2  21492  thlval  21650  islindf4  21793  psrval  21871  opsrval  22001  opsrval2  22003  matval  22355  mat1dimmul  22420  mat1dimcrng  22421  mat1scmat  22483  mdet0pr  22536  m1detdiag  22541  txkgen  23596  pt1hmeo  23750  xpstopnlem1  23753  xpstopnlem2  23755  tusval  24209  tmsval  24425  tngval  24583  om1val  24986  pi1xfrcnvlem  25012  pi1xfrcnv  25013  dchrval  27201  nosupbnd2lem1  27683  noinfbnd2lem1  27698  seqseq123d  28282  om2noseqrdg  28300  noseqrdgsuc  28304  ttgval  28947  eengv  29052  uspgr1ewop  29321  usgr2v1e2w  29325  1loopgruspgr  29574  1egrvtxdg1r  29584  1egrvtxdg0  29585  eupth2lem3lem3  30305  eupth2  30314  wlkl0  30442  br8d  32686  fresunsn  32703  elrgspnlem2  33325  rlocval  33341  rlocf1  33355  resvval  33410  opprabs  33563  idlsrgval  33584  extvfvcl  33701  resssra  33743  smatfval  33952  smatrcl  33953  smatlem  33954  qqhval  34129  bnj66  35016  bnj1234  35169  bnj1296  35177  bnj1450  35206  bnj1463  35211  bnj1501  35223  bnj1523  35227  subfacp1lem5  35378  cvmliftlem10  35488  cvmlift2lem12  35508  goaleq12d  35545  sategoelfvb  35613  msubffval  35717  msubfval  35718  elmsubrn  35722  msubrn  35723  msubco  35725  br8  35950  br6  35951  btwnouttr2  36216  brfs  36273  btwnconn1lem11  36291  cbvoprab3davw  36467  bj-dfid2ALT  37266  bj-endval  37520  csbfinxpg  37593  finixpnum  37806  ldualset  39385  tgrpfset  41004  tgrpset  41005  erngfset  41059  erngset  41060  erngfset-rN  41067  erngset-rN  41068  dvafset  41264  dvaset  41265  dvhfset  41340  dvhset  41341  dvhfvadd  41351  dvhopvadd2  41354  dib1dim2  41428  dicvscacl  41451  cdlemn6  41462  dihopelvalcpre  41508  dih1dimatlem  41589  hdmapfval  42087  hlhilset  42194  mendval  43421  mnringvald  44454  ovolval4lem1  46893  ovolval4lem2  46894  ovnovollem3  46902  isubgrvtxuhgr  48110  isubgr0uhgr  48119  stgrfv  48199  gpgov  48288  gpgprismgriedgdmss  48298  gpgvtx0  48299  gpgvtx1  48300  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  gpgedg2ov  48312  gpgedg2iv  48313  gpg3kgrtriexlem6  48334  gpg3kgrtriex  48335  gpgprismgr4cycllem3  48343  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5  48369  gpg5edgnedg  48376  rngcvalALTV  48511  ringcvalALTV  48535  zlmodzxzsub  48606  lmod1zr  48739  2arymaptf  48898  discsubc  49309  2oppf  49377  upfval2  49422  upfval3  49423  isuplem  49424  uptpos  49443  uptr2  49466  dfswapf2  49506  oppc1stf  49533  oppc2ndf  49534  fucolid  49606  fucorid  49607  precofval2  49614  prcofval  49623  isinito2lem  49743  termcfuncval  49777  prstcval  49796  mndtcval  49824  lanup  49886  coccom  49909  iscmd  49911