Theorem preq1d 4744

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypothesis

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
preq1d	⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Proof of Theorem preq1d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq1 4738	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1537  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  propeqop  5517  opthwiener  5524  fprg  7175  fprb  7214  fnpr2g  7230  dif1en  9199  dif1enOLD  9201  dfac2b  10169  symg2bas  19425  crctcshwlkn0lem6  29845  wwlksnredwwlkn  29925  wwlksnextprop  29942  clwwlk1loop  30017  clwlkclwwlklem2fv1  30024  clwlkclwwlklem2fv2  30025  clwlkclwwlklem2a  30027  clwlkclwwlklem3  30030  clwwisshclwwslem  30043  clwwlknlbonbgr1  30068  clwwlkn1  30070  frcond1  30295  frgr1v  30300  nfrgr2v  30301  frgr3v  30304  n4cyclfrgr  30320  2clwwlk2clwwlklem  30375  wopprc  43019  mnurndlem1  44277  grtriclwlk3  47850  isubgr3stgrlem4  47872  2arymaptf1  48503  rrx2xpref1o  48568