Theorem preq2d 4745

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  opeq2  4879  opthwiener  5524  fprg  7175  fprb  7214  fnprb  7228  fnpr2g  7230  opthreg  9656  fzosplitprm1  13813  s2prop  14943  gsumprval  18714  indislem  23023  isconn  23437  hmphindis  23821  wilthlem2  27127  ispth  29756  wwlksnredwwlkn  29925  wwlksnextfun  29928  wwlksnextinj  29929  wwlksnextsurj  29930  wwlksnextbij  29932  clwlkclwwlklem2a1  30021  clwlkclwwlklem2a4  30026  clwlkclwwlklem2  30029  clwwisshclwwslemlem  30042  clwwlkn2  30073  clwwlkf  30076  clwwlknonex2lem1  30136  eupth2lem3lem3  30259  eupth2  30268  frcond1  30295  nfrgr2v  30301  frgr3v  30304  n4cyclfrgr  30320  measxun2  34191  altopthsn  35943  mapdindp4  41706  clnbgrgrimlem  47839  gpgov  47937  2arymaptf1  48503  rrx2xpref1o  48568