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  4834  opthwiener  5487  fprg  7142  fprb  7182  fnprb  7196  fnpr2g  7198  opthreg  9575  fzosplitprm1  13795  s2prop  14932  chnccat  18670  gsumprval  18734  indislem  23114  isconn  23527  hmphindis  23911  wilthlem2  27187  ispth  29975  wwlksnredwwlkn  30149  wwlksnextfun  30152  wwlksnextinj  30153  wwlksnextsurj  30154  wwlksnextbij  30156  clwlkclwwlklem2a1  30248  clwlkclwwlklem2a4  30253  clwlkclwwlklem2  30256  clwwisshclwwslemlem  30269  clwwlkn2  30300  clwwlkf  30303  clwwlknonex2lem1  30363  eupth2lem3lem3  30486  eupth2  30495  frcond1  30522  nfrgr2v  30528  frgr3v  30531  n4cyclfrgr  30547  measxun2  34512  altopthsn  36319  mapdindp4  42354  clnbgrgrimlem  48554  gpgov  48663  gpgprismgriedgdmss  48673  gpgedg2ov  48687  gpgedg2iv  48688  gpg3kgrtriexlem6  48709  gpgprismgr4cycllem3  48718  grlimedgnedg  48752  2arymaptf1  49285  rrx2xpref1o  49350