Theorem preq2d 4702

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

Syntax hints:   → wi 4   = wceq 1563  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  opeq2  4835  opthwiener  5488  fprg  7142  fprb  7182  fnprb  7196  fnpr2g  7198  opthreg  9575  fzosplitprm1  13798  s2prop  14934  chnccat  18672  gsumprval  18736  indislem  23118  isconn  23531  hmphindis  23915  wilthlem2  27191  ispth  29979  wwlksnredwwlkn  30153  wwlksnextfun  30156  wwlksnextinj  30157  wwlksnextsurj  30158  wwlksnextbij  30160  clwlkclwwlklem2a1  30252  clwlkclwwlklem2a4  30257  clwlkclwwlklem2  30260  clwwisshclwwslemlem  30273  clwwlkn2  30304  clwwlkf  30307  clwwlknonex2lem1  30367  eupth2lem3lem3  30490  eupth2  30499  frcond1  30526  nfrgr2v  30532  frgr3v  30535  n4cyclfrgr  30551  measxun2  34517  altopthsn  36324  mapdindp4  42359  clnbgrgrimlem  48553  gpgov  48662  gpgprismgriedgdmss  48672  gpgedg2ov  48686  gpgedg2iv  48687  gpg3kgrtriexlem6  48708  gpgprismgr4cycllem3  48717  grlimedgnedg  48751  2arymaptf1  49284  rrx2xpref1o  49349