Theorem preq2d 4673

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

Syntax hints:   → wi 4   = wceq 1539  {cpr 4560

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-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  opeq2  4802  opthwiener  5422  fprg  7009  fprb  7051  fnprb  7066  fnpr2g  7068  opthreg  9306  fzosplitprm1  13425  s2prop  14548  gsumprval  18287  indislem  22058  isconn  22472  hmphindis  22856  wilthlem2  26123  ispth  27992  wwlksnredwwlkn  28161  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextsurj  28166  wwlksnextbij  28168  clwlkclwwlklem2a1  28257  clwlkclwwlklem2a4  28262  clwlkclwwlklem2  28265  clwwisshclwwslemlem  28278  clwwlkn2  28309  clwwlkf  28312  clwwlknonex2lem1  28372  eupth2lem3lem3  28495  eupth2  28504  frcond1  28531  nfrgr2v  28537  frgr3v  28540  n4cyclfrgr  28556  measxun2  32078  altopthsn  34190  mapdindp4  39664  isomuspgrlem2d  45171  2arymaptf1  45887  rrx2xpref1o  45952