Theorem preq1d 4672

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

Syntax hints:   → wi 4   = wceq 1539  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  propeqop  5415  opthwiener  5422  fprg  7009  fprb  7051  fnpr2g  7068  dif1en  8907  dfac2b  9817  symg2bas  18915  crctcshwlkn0lem6  28081  wwlksnredwwlkn  28161  wwlksnextprop  28178  clwwlk1loop  28253  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a  28263  clwlkclwwlklem3  28266  clwwisshclwwslem  28279  clwwlknlbonbgr1  28304  clwwlkn1  28306  frcond1  28531  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  n4cyclfrgr  28556  2clwwlk2clwwlklem  28611  wopprc  40768  mnurndlem1  41788  isomuspgrlem2d  45171  2arymaptf1  45887  rrx2xpref1o  45952