Theorem preq2d 4701

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  opeq2  4834  opthwiener  5487  fprg  7151  fprb  7191  fnprb  7206  fnpr2g  7208  opthreg  9603  fzosplitprm1  13893  s2prop  15038  chnccat  18780  gsumprval  18857  indislem  23298  isconn  23711  hmphindis  24096  wilthlem2  27378  ispth  30288  wwlksnredwwlkn  30466  wwlksnextfun  30469  wwlksnextinj  30470  wwlksnextsurj  30471  wwlksnextbij  30473  clwlkclwwlklem2a1  30565  clwlkclwwlklem2a4  30570  clwlkclwwlklem2  30573  clwwisshclwwslemlem  30586  clwwlkn2  30617  clwwlkf  30620  clwwlknonex2lem1  30680  eupth2lem3lem3  30813  eupth2  30822  frcond1  30849  nfrgr2v  30855  frgr3v  30858  n4cyclfrgr  30874  measxun2  34825  altopthsn  36696  mapdindp4  42748  clnbgrgrimlem  48975  gpgov  49084  gpgprismgriedgdmss  49094  gpgedg2ov  49108  gpgedg2iv  49109  gpg3kgrtriexlem6  49130  gpgprismgr4cycllem3  49139  grlimedgnedg  49173  2arymaptf1  49709  rrx2xpref1o  49774