Theorem preq1d 4698

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  propeqop  5463  opthwiener  5470  fprg  7110  fprb  7150  fnpr2g  7166  dif1en  9098  dfac2b  10053  symg2bas  19334  crctcshwlkn0lem6  29900  wwlksnredwwlkn  29980  wwlksnextprop  29997  clwwlk1loop  30075  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2a  30085  clwlkclwwlklem3  30088  clwwisshclwwslem  30101  clwwlknlbonbgr1  30126  clwwlkn1  30128  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  n4cyclfrgr  30378  2clwwlk2clwwlklem  30433  wopprc  43381  mnurndlem1  44631  grtriclwlk3  48299  isubgr3stgrlem4  48323  gpgedgiov  48419  gpgedg2ov  48420  gpgedg2iv  48421  pgnbgreunbgrlem5lem1  48474  pgnbgreunbgrlem5lem2  48475  pgnbgreunbgrlem5lem3  48476  grlimedgnedg  48485  2arymaptf1  49007  rrx2xpref1o  49072