Theorem preq2d 4704

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4589

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  opeq2  4837  opthwiener  5495  fprg  7156  fprb  7196  fnprb  7211  fnpr2g  7213  opthreg  9601  fzosplitprm1  13838  s2prop  14982  chnccat  18720  gsumprval  18796  indislem  23231  isconn  23644  hmphindis  24029  wilthlem2  27313  ispth  30193  wwlksnredwwlkn  30371  wwlksnextfun  30374  wwlksnextinj  30375  wwlksnextsurj  30376  wwlksnextbij  30378  clwlkclwwlklem2a1  30470  clwlkclwwlklem2a4  30475  clwlkclwwlklem2  30478  clwwisshclwwslemlem  30491  clwwlkn2  30522  clwwlkf  30525  clwwlknonex2lem1  30585  eupth2lem3lem3  30718  eupth2  30727  frcond1  30754  nfrgr2v  30760  frgr3v  30763  n4cyclfrgr  30779  measxun2  34729  altopthsn  36549  mapdindp4  42604  clnbgrgrimlem  48857  gpgov  48966  gpgprismgriedgdmss  48976  gpgedg2ov  48990  gpgedg2iv  48991  gpg3kgrtriexlem6  49012  gpgprismgr4cycllem3  49021  grlimedgnedg  49055  2arymaptf1  49591  rrx2xpref1o  49656