Theorem preq2d 4743

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3952  df-sn 4628  df-pr 4630

This theorem is referenced by:  opeq2  4873  opthwiener  5513  fprg  7149  fprb  7191  fnprb  7206  fnpr2g  7208  opthreg  9609  fzosplitprm1  13738  s2prop  14854  gsumprval  18603  indislem  22494  isconn  22908  hmphindis  23292  wilthlem2  26562  ispth  28969  wwlksnredwwlkn  29138  wwlksnextfun  29141  wwlksnextinj  29142  wwlksnextsurj  29143  wwlksnextbij  29145  clwlkclwwlklem2a1  29234  clwlkclwwlklem2a4  29239  clwlkclwwlklem2  29242  clwwisshclwwslemlem  29255  clwwlkn2  29286  clwwlkf  29289  clwwlknonex2lem1  29349  eupth2lem3lem3  29472  eupth2  29481  frcond1  29508  nfrgr2v  29514  frgr3v  29517  n4cyclfrgr  29533  measxun2  33196  altopthsn  34921  mapdindp4  40582  isomuspgrlem2d  46485  2arymaptf1  47292  rrx2xpref1o  47357