Theorem preq2d 4219

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

Syntax hints:   → wi 4   = wceq 1475  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  opeq2  4341  opthwiener  4901  fprg  6327  fnprb  6377  fnpr2g  6379  opthreg  8398  s2prop  13502  gsumprval  17104  indislem  20614  iscon  21026  hmphindis  21410  wilthlem2  24595  ispth  26098  1pthonlem2  26120  2pthoncl  26133  wwlknredwwlkn  26254  wwlkextfun  26257  wwlkextinj  26258  wwlkextsur  26259  wwlkextbij  26261  clwwlkn2  26303  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem1  26315  clwwlkf  26322  clwwisshclwwlem1  26333  eupath2lem3  26506  eupath2  26507  frgraunss  26522  frgra2v  26526  frgra3v  26529  n4cyclfrgra  26545  extwwlkfablem1  26601  extwwlkfablem2  26605  measxun2  29600  fprb  30916  altopthsn  31238  mapdindp4  36030  isPth  40929  wwlksnredwwlkn  41101  wwlksnextfun  41104  wwlksnextinj  41105  wwlksnextsur  41106  wwlksnextbij  41108  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a4  41206  clwlkclwwlklem2  41209  clwwlksn2  41217  clwwlksf  41222  clwwisshclwwslemlem  41233  eupth2lem3lem3  41398  eupth2  41407  frcond1  41438  nfrgr2v  41442  frgr3v  41445  n4cyclfrgr  41461  av-extwwlkfablem1  41508