Theorem preq1d 4697

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

Syntax hints:   → wi 4   = wceq 1559  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4582  df-pr 4584

This theorem is referenced by:  propeqop  5475  opthwiener  5482  fprg  7134  fprb  7174  fnpr2g  7190  dif1en  9126  dfac2b  10084  symg2bas  19416  crctcshwlkn0lem6  29961  wwlksnredwwlkn  30041  wwlksnextprop  30058  clwwlk1loop  30136  clwlkclwwlklem2fv1  30143  clwlkclwwlklem2fv2  30144  clwlkclwwlklem2a  30146  clwlkclwwlklem3  30149  clwwisshclwwslem  30162  clwwlknlbonbgr1  30187  clwwlkn1  30189  frcond1  30414  frgr1v  30419  nfrgr2v  30420  frgr3v  30423  n4cyclfrgr  30439  2clwwlk2clwwlklem  30494  wopprc  43571  mnurndlem1  44821  grtriclwlk3  48531  isubgr3stgrlem4  48555  gpgedgiov  48651  gpgedg2ov  48652  gpgedg2iv  48653  pgnbgreunbgrlem5lem1  48706  pgnbgreunbgrlem5lem2  48707  pgnbgreunbgrlem5lem3  48708  grlimedgnedg  48717  2arymaptf1  49239  rrx2xpref1o  49304