Theorem preq2d 4692

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypothesis

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
preq2d	⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq2 4686	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1541  {cpr 4577

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578

This theorem is referenced by:  opeq2  4825  opthwiener  5457  fprg  7094  fprb  7134  fnprb  7148  fnpr2g  7150  opthreg  9515  fzosplitprm1  13680  s2prop  14816  chnccat  18534  gsumprval  18598  indislem  22916  isconn  23329  hmphindis  23713  wilthlem2  27007  ispth  29701  wwlksnredwwlkn  29875  wwlksnextfun  29878  wwlksnextinj  29879  wwlksnextsurj  29880  wwlksnextbij  29882  clwlkclwwlklem2a1  29974  clwlkclwwlklem2a4  29979  clwlkclwwlklem2  29982  clwwisshclwwslemlem  29995  clwwlkn2  30026  clwwlkf  30029  clwwlknonex2lem1  30089  eupth2lem3lem3  30212  eupth2  30221  frcond1  30248  nfrgr2v  30254  frgr3v  30257  n4cyclfrgr  30273  measxun2  34244  altopthsn  36026  mapdindp4  41843  clnbgrgrimlem  48058  gpgov  48167  gpgprismgriedgdmss  48177  gpgedg2ov  48191  gpgedg2iv  48192  gpg3kgrtriexlem6  48213  gpgprismgr4cycllem3  48222  grlimedgnedg  48256  2arymaptf1  48779  rrx2xpref1o  48844