Theorem preq2d 4699

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  opeq2  4832  opthwiener  5470  fprg  7110  fprb  7150  fnprb  7164  fnpr2g  7166  opthreg  9539  fzosplitprm1  13706  s2prop  14842  chnccat  18561  gsumprval  18625  indislem  22956  isconn  23369  hmphindis  23753  wilthlem2  27047  ispth  29806  wwlksnredwwlkn  29980  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextsurj  29985  wwlksnextbij  29987  clwlkclwwlklem2a1  30079  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  clwwisshclwwslemlem  30100  clwwlkn2  30131  clwwlkf  30134  clwwlknonex2lem1  30194  eupth2lem3lem3  30317  eupth2  30326  frcond1  30353  nfrgr2v  30359  frgr3v  30362  n4cyclfrgr  30378  measxun2  34387  altopthsn  36174  mapdindp4  42093  clnbgrgrimlem  48287  gpgov  48396  gpgprismgriedgdmss  48406  gpgedg2ov  48420  gpgedg2iv  48421  gpg3kgrtriexlem6  48442  gpgprismgr4cycllem3  48451  grlimedgnedg  48485  2arymaptf1  49007  rrx2xpref1o  49072