Theorem preq2d 4739

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

Syntax hints:   → wi 4   = wceq 1539  {cpr 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-sn 4626  df-pr 4628

This theorem is referenced by:  opeq2  4873  opthwiener  5518  fprg  7174  fprb  7215  fnprb  7229  fnpr2g  7231  opthreg  9659  fzosplitprm1  13817  s2prop  14947  gsumprval  18702  indislem  23008  isconn  23422  hmphindis  23806  wilthlem2  27113  ispth  29742  wwlksnredwwlkn  29916  wwlksnextfun  29919  wwlksnextinj  29920  wwlksnextsurj  29921  wwlksnextbij  29923  clwlkclwwlklem2a1  30012  clwlkclwwlklem2a4  30017  clwlkclwwlklem2  30020  clwwisshclwwslemlem  30033  clwwlkn2  30064  clwwlkf  30067  clwwlknonex2lem1  30127  eupth2lem3lem3  30250  eupth2  30259  frcond1  30286  nfrgr2v  30292  frgr3v  30295  n4cyclfrgr  30311  measxun2  34212  altopthsn  35963  mapdindp4  41726  clnbgrgrimlem  47906  gpgov  48006  gpg3kgrtriexlem6  48049  2arymaptf1  48579  rrx2xpref1o  48644