Theorem preq2d 4704

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  opeq2  4838  opthwiener  5474  fprg  7127  fprb  7168  fnprb  7182  fnpr2g  7184  opthreg  9571  fzosplitprm1  13738  s2prop  14873  gsumprval  18615  indislem  22887  isconn  23300  hmphindis  23684  wilthlem2  26979  ispth  29651  wwlksnredwwlkn  29825  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextsurj  29830  wwlksnextbij  29832  clwlkclwwlklem2a1  29921  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  clwwisshclwwslemlem  29942  clwwlkn2  29973  clwwlkf  29976  clwwlknonex2lem1  30036  eupth2lem3lem3  30159  eupth2  30168  frcond1  30195  nfrgr2v  30201  frgr3v  30204  n4cyclfrgr  30220  measxun2  34200  altopthsn  35949  mapdindp4  41717  clnbgrgrimlem  47930  gpgov  48030  gpgprismgriedgdmss  48040  gpgedg2ov  48054  gpgedg2iv  48055  gpg3kgrtriexlem6  48076  gpgprismgr4cycllem3  48084  2arymaptf1  48639  rrx2xpref1o  48704