Theorem preq2d 4693

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  opeq2  4826  opthwiener  5454  fprg  7088  fprb  7128  fnprb  7142  fnpr2g  7144  opthreg  9508  fzosplitprm1  13675  s2prop  14811  chnccat  18529  gsumprval  18593  indislem  22913  isconn  23326  hmphindis  23710  wilthlem2  27004  ispth  29697  wwlksnredwwlkn  29871  wwlksnextfun  29874  wwlksnextinj  29875  wwlksnextsurj  29876  wwlksnextbij  29878  clwlkclwwlklem2a1  29967  clwlkclwwlklem2a4  29972  clwlkclwwlklem2  29975  clwwisshclwwslemlem  29988  clwwlkn2  30019  clwwlkf  30022  clwwlknonex2lem1  30082  eupth2lem3lem3  30205  eupth2  30214  frcond1  30241  nfrgr2v  30247  frgr3v  30250  n4cyclfrgr  30266  measxun2  34218  altopthsn  35994  mapdindp4  41761  clnbgrgrimlem  47963  gpgov  48072  gpgprismgriedgdmss  48082  gpgedg2ov  48096  gpgedg2iv  48097  gpg3kgrtriexlem6  48118  gpgprismgr4cycllem3  48127  grlimedgnedg  48161  2arymaptf1  48684  rrx2xpref1o  48749