Theorem preq1d 4710

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  propeqop  5495  opthwiener  5502  fprg  7159  fprb  7199  fnpr2g  7215  dif1en  9156  dfac2b  10133  symg2bas  19494  crctcshwlkn0lem6  30201  wwlksnredwwlkn  30281  wwlksnextprop  30298  clwwlk1loop  30376  clwlkclwwlklem2fv1  30383  clwlkclwwlklem2fv2  30384  clwlkclwwlklem2a  30386  clwlkclwwlklem3  30389  clwwisshclwwslem  30402  clwwlknlbonbgr1  30427  clwwlkn1  30429  frcond1  30654  frgr1v  30659  nfrgr2v  30660  frgr3v  30663  n4cyclfrgr  30679  2clwwlk2clwwlklem  30734  wopprc  43798  mnurndlem1  45032  grtriclwlk3  48751  isubgr3stgrlem4  48775  gpgedgiov  48871  gpgedg2ov  48872  gpgedg2iv  48873  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  grlimedgnedg  48937  2arymaptf1  49474  rrx2xpref1o  49539