Theorem preq2d 4697

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  opeq2  4830  opthwiener  5462  fprg  7100  fprb  7140  fnprb  7154  fnpr2g  7156  opthreg  9527  fzosplitprm1  13694  s2prop  14830  chnccat  18549  gsumprval  18613  indislem  22944  isconn  23357  hmphindis  23741  wilthlem2  27035  ispth  29794  wwlksnredwwlkn  29968  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextsurj  29973  wwlksnextbij  29975  clwlkclwwlklem2a1  30067  clwlkclwwlklem2a4  30072  clwlkclwwlklem2  30075  clwwisshclwwslemlem  30088  clwwlkn2  30119  clwwlkf  30122  clwwlknonex2lem1  30182  eupth2lem3lem3  30305  eupth2  30314  frcond1  30341  nfrgr2v  30347  frgr3v  30350  n4cyclfrgr  30366  measxun2  34367  altopthsn  36155  mapdindp4  41979  clnbgrgrimlem  48175  gpgov  48284  gpgprismgriedgdmss  48294  gpgedg2ov  48308  gpgedg2iv  48309  gpg3kgrtriexlem6  48330  gpgprismgr4cycllem3  48339  grlimedgnedg  48373  2arymaptf1  48895  rrx2xpref1o  48960