Theorem preq2d 4464

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

Syntax hints:   → wi 4   = wceq 1653  {cpr 4370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-un 3774  df-sn 4369  df-pr 4371

This theorem is referenced by:  opeq2  4594  opthwiener  5170  fprg  6650  fnprb  6701  fnpr2g  6703  opthreg  8763  opthregOLD  8765  fzosplitprm1  12833  s2prop  13992  gsumprval  17596  indislem  21133  isconn  21545  hmphindis  21929  wilthlem2  25147  ispth  26977  wwlksnredwwlkn  27165  wwlksnredwwlknOLD  27166  wwlksnextfun  27170  wwlksnextinj  27171  wwlksnextsurj  27172  wwlksnextfunOLD  27175  wwlksnextinjOLD  27176  wwlksnextsurOLD  27177  wwlksnextbij  27179  wwlksnextbijOLD  27180  clwlkclwwlklem2a1  27285  clwlkclwwlklem2a4  27290  clwlkclwwlklem2  27293  clwwisshclwwslemlem  27315  clwwlkn2  27353  clwwlkfOLD  27356  clwwlkf  27361  clwwlknonex2lem1  27447  eupth2lem3lem3  27575  eupth2  27584  frcond1  27615  nfrgr2v  27621  frgr3v  27624  n4cyclfrgr  27640  extwwlkfablem1OLD  27691  measxun2  30789  fprb  32183  altopthsn  32581  mapdindp4  37744  isomuspgrlem2d  42501