Theorem preq2d 4679

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

Syntax hints:   → wi 4   = wceq 1537  {cpr 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-un 3894  df-sn 4565  df-pr 4567

This theorem is referenced by:  opeq2  4807  opthwiener  5431  fprg  7047  fprb  7089  fnprb  7104  fnpr2g  7106  opthreg  9404  fzosplitprm1  13525  s2prop  14648  gsumprval  18400  indislem  22178  isconn  22592  hmphindis  22976  wilthlem2  26246  ispth  28119  wwlksnredwwlkn  28288  wwlksnextfun  28291  wwlksnextinj  28292  wwlksnextsurj  28293  wwlksnextbij  28295  clwlkclwwlklem2a1  28384  clwlkclwwlklem2a4  28389  clwlkclwwlklem2  28392  clwwisshclwwslemlem  28405  clwwlkn2  28436  clwwlkf  28439  clwwlknonex2lem1  28499  eupth2lem3lem3  28622  eupth2  28631  frcond1  28658  nfrgr2v  28664  frgr3v  28667  n4cyclfrgr  28683  measxun2  32206  altopthsn  34291  mapdindp4  39763  isomuspgrlem2d  45323  2arymaptf1  46039  rrx2xpref1o  46104