Theorem preq2d 4707

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

Syntax hints:   → wi 4   = wceq 1570  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  opeq2  4840  opthwiener  5499  fprg  7154  fprb  7194  fnprb  7208  fnpr2g  7210  opthreg  9588  fzosplitprm1  13809  s2prop  14946  chnccat  18683  gsumprval  18747  indislem  23138  isconn  23551  hmphindis  23935  wilthlem2  27214  ispth  30051  wwlksnredwwlkn  30225  wwlksnextfun  30228  wwlksnextinj  30229  wwlksnextsurj  30230  wwlksnextbij  30232  clwlkclwwlklem2a1  30324  clwlkclwwlklem2a4  30329  clwlkclwwlklem2  30332  clwwisshclwwslemlem  30345  clwwlkn2  30376  clwwlkf  30379  clwwlknonex2lem1  30439  eupth2lem3lem3  30562  eupth2  30571  frcond1  30598  nfrgr2v  30604  frgr3v  30607  n4cyclfrgr  30623  measxun2  34581  altopthsn  36434  mapdindp4  42478  clnbgrgrimlem  48681  gpgov  48790  gpgprismgriedgdmss  48800  gpgedg2ov  48814  gpgedg2iv  48815  gpg3kgrtriexlem6  48836  gpgprismgr4cycllem3  48845  grlimedgnedg  48879  2arymaptf1  49416  rrx2xpref1o  49481