Theorem preq1d 4691

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

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

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4576  df-pr 4578

This theorem is referenced by:  propeqop  5450  opthwiener  5457  fprg  7094  fprb  7134  fnpr2g  7150  dif1en  9078  dfac2b  10029  symg2bas  19307  crctcshwlkn0lem6  29795  wwlksnredwwlkn  29875  wwlksnextprop  29892  clwwlk1loop  29970  clwlkclwwlklem2fv1  29977  clwlkclwwlklem2fv2  29978  clwlkclwwlklem2a  29980  clwlkclwwlklem3  29983  clwwisshclwwslem  29996  clwwlknlbonbgr1  30021  clwwlkn1  30023  frcond1  30248  frgr1v  30253  nfrgr2v  30254  frgr3v  30257  n4cyclfrgr  30273  2clwwlk2clwwlklem  30328  wopprc  43148  mnurndlem1  44399  grtriclwlk3  48070  isubgr3stgrlem4  48094  gpgedgiov  48190  gpgedg2ov  48191  gpgedg2iv  48192  pgnbgreunbgrlem5lem1  48245  pgnbgreunbgrlem5lem2  48246  pgnbgreunbgrlem5lem3  48247  grlimedgnedg  48256  2arymaptf1  48779  rrx2xpref1o  48844