Theorem preq2d 4411

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

Syntax hints:   → wi 4   = wceq 1631  {cpr 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-un 3728  df-sn 4317  df-pr 4319

This theorem is referenced by:  opeq2  4540  opthwiener  5107  fprg  6565  fnprb  6616  fnpr2g  6618  opthreg  8677  opthregOLD  8679  fzosplitprm1  12786  s2prop  13861  gsumprval  17489  indislem  21025  isconn  21437  hmphindis  21821  wilthlem2  25016  ispth  26854  wwlksnredwwlkn  27039  wwlksnextfun  27042  wwlksnextinj  27043  wwlksnextsur  27044  wwlksnextbij  27046  clwlkclwwlklem2a1  27142  clwlkclwwlklem2a4  27147  clwlkclwwlklem2  27150  clwwisshclwwslemlem  27163  clwwlkn2  27200  clwwlkf  27203  clwwlknonex2lem1  27283  eupth2lem3lem3  27410  eupth2  27419  frcond1  27448  nfrgr2v  27454  frgr3v  27457  n4cyclfrgr  27473  extwwlkfablem1OLD  27524  measxun2  30613  fprb  32007  altopthsn  32405  mapdindp4  37533