Theorem preq1d 4703

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  propeqop  5467  opthwiener  5474  fprg  7127  fprb  7168  fnpr2g  7184  dif1en  9124  dif1enOLD  9126  dfac2b  10084  symg2bas  19323  crctcshwlkn0lem6  29745  wwlksnredwwlkn  29825  wwlksnextprop  29842  clwwlk1loop  29917  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a  29927  clwlkclwwlklem3  29930  clwwisshclwwslem  29943  clwwlknlbonbgr1  29968  clwwlkn1  29970  frcond1  30195  frgr1v  30200  nfrgr2v  30201  frgr3v  30204  n4cyclfrgr  30220  2clwwlk2clwwlklem  30275  wopprc  43019  mnurndlem1  44270  grtriclwlk3  47941  isubgr3stgrlem4  47965  gpgedgiov  48053  gpgedg2ov  48054  gpgedg2iv  48055  pgnbgreunbgrlem5lem1  48107  pgnbgreunbgrlem5lem2  48108  pgnbgreunbgrlem5lem3  48109  2arymaptf1  48639  rrx2xpref1o  48704