Theorem preq2d 4698

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

Syntax hints:   → wi 4   = wceq 1559  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4582  df-pr 4584

This theorem is referenced by:  opeq2  4831  opthwiener  5482  fprg  7134  fprb  7174  fnprb  7188  fnpr2g  7190  opthreg  9570  fzosplitprm1  13781  s2prop  14917  chnccat  18641  gsumprval  18705  indislem  23040  isconn  23453  hmphindis  23837  wilthlem2  27110  ispth  29867  wwlksnredwwlkn  30041  wwlksnextfun  30044  wwlksnextinj  30045  wwlksnextsurj  30046  wwlksnextbij  30048  clwlkclwwlklem2a1  30140  clwlkclwwlklem2a4  30145  clwlkclwwlklem2  30148  clwwisshclwwslemlem  30161  clwwlkn2  30192  clwwlkf  30195  clwwlknonex2lem1  30255  eupth2lem3lem3  30378  eupth2  30387  frcond1  30414  nfrgr2v  30420  frgr3v  30423  n4cyclfrgr  30439  measxun2  34468  altopthsn  36275  mapdindp4  42311  clnbgrgrimlem  48519  gpgov  48628  gpgprismgriedgdmss  48638  gpgedg2ov  48652  gpgedg2iv  48653  gpg3kgrtriexlem6  48674  gpgprismgr4cycllem3  48683  grlimedgnedg  48717  2arymaptf1  49239  rrx2xpref1o  49304