Theorem opeq2d 4880

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  dfid2  5580  funopsn  7168  fmptsng  7188  fmptsnd  7189  fvproj  8159  tfrlem11  8428  seqomlem0  8489  seqomlem1  8490  seqomlem4  8493  seqomeq12  8494  fundmen  9071  dif1en  9200  dif1enOLD  9202  unxpdomlem1  9286  mulcanenq  11000  elreal2  11172  om2uzrdg  13997  uzrdgsuci  14001  seqeq2  14046  seqeq3  14047  s1val  14636  s1eq  14638  swrdlsw  14705  pfxpfx  14746  swrdccat  14773  swrdccat3blem  14777  swrdccat3b  14778  pfxccatin12d  14783  swrds2  14979  swrds2m  14980  swrd2lsw  14991  eucalgval  16619  setsidvald  17236  ressval  17277  ressress  17293  prdsval  17500  imasval  17556  imasaddvallem  17574  xpsfval  17611  xpsval  17615  cidval  17720  iscatd2  17724  oppcval  17756  ismon  17777  rescval  17871  idfucl  17926  funcres  17941  idfusubc0  17944  idfusubc  17945  fucval  18006  fucpropd  18025  setcval  18122  catcval  18145  estrcval  18168  xpcval  18222  1stfcl  18242  2ndfcl  18243  curf12  18272  curf2val  18275  curfcl  18277  hofcl  18304  oduval  18333  ipoval  18575  frmdval  18864  efmnd  18883  oppgval  19365  symgvalstruct  19414  symgvalstructOLD  19415  efgmval  19730  efgmnvl  19732  efgi  19737  frgpup3lem  19795  dprd2da  20062  dmdprdpr  20069  dprdpr  20070  pgpfaclem1  20101  mgpval  20140  mgpress  20147  opprval  20335  sraval  21174  rlmval2  21199  pzriprnglem10  21501  zlmval  21526  znval  21550  znval2  21552  thlval  21713  islindf4  21858  psrval  21935  opsrval  22064  opsrval2  22066  matval  22415  mat1dimmul  22482  mat1dimcrng  22483  mat1scmat  22545  mdet0pr  22598  m1detdiag  22603  txkgen  23660  pt1hmeo  23814  xpstopnlem1  23817  xpstopnlem2  23819  tusval  24274  tmsval  24493  tngval  24652  om1val  25063  pi1xfrcnvlem  25089  pi1xfrcnv  25090  dchrval  27278  nosupbnd2lem1  27760  noinfbnd2lem1  27775  seqseq123d  28292  om2noseqrdg  28310  noseqrdgsuc  28314  ttgval  28883  ttgvalOLD  28884  eengv  28994  uspgr1ewop  29265  usgr2v1e2w  29269  1loopgruspgr  29518  1egrvtxdg1r  29528  1egrvtxdg0  29529  eupth2lem3lem3  30249  eupth2  30258  wlkl0  30386  br8d  32622  elrgspnlem2  33247  rlocval  33263  rlocf1  33277  resvval  33353  opprabs  33510  idlsrgval  33531  resssra  33638  smatfval  33794  smatrcl  33795  smatlem  33796  qqhval  33973  bnj66  34874  bnj1234  35027  bnj1296  35035  bnj1450  35064  bnj1463  35069  bnj1501  35081  bnj1523  35085  subfacp1lem5  35189  cvmliftlem10  35299  cvmlift2lem12  35319  goaleq12d  35356  sategoelfvb  35424  msubffval  35528  msubfval  35529  elmsubrn  35533  msubrn  35534  msubco  35536  br8  35756  br6  35757  btwnouttr2  36023  brfs  36080  btwnconn1lem11  36098  cbvoprab3davw  36274  bj-dfid2ALT  37066  bj-endval  37316  csbfinxpg  37389  finixpnum  37612  ldualset  39126  tgrpfset  40746  tgrpset  40747  erngfset  40801  erngset  40802  erngfset-rN  40809  erngset-rN  40810  dvafset  41006  dvaset  41007  dvhfset  41082  dvhset  41083  dvhfvadd  41093  dvhopvadd2  41096  dib1dim2  41170  dicvscacl  41193  cdlemn6  41204  dihopelvalcpre  41250  dih1dimatlem  41331  hdmapfval  41829  hlhilset  41936  mendval  43191  mnringvald  44227  ovolval4lem1  46664  ovolval4lem2  46665  ovnovollem3  46673  isubgrvtxuhgr  47850  isubgr0uhgr  47859  stgrfv  47920  gpgov  48001  gpgvtx0  48008  gpgvtx1  48009  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg3kgrtriexlem6  48044  gpg3kgrtriex  48045  rngcvalALTV  48181  ringcvalALTV  48205  zlmodzxzsub  48276  lmod1zr  48410  2arymaptf  48573  upfval2  48934  upfval3  48935  isuplem  48936  dfswapf2  48967  fucolid  49056  fucorid  49057  precofval2  49064  prstcval  49153  mndtcval  49176