Theorem preq1d 4700

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

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

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  propeqop  5479  opthwiener  5487  fprg  7151  fprb  7191  fnpr2g  7208  dif1en  9161  dfac2b  10190  symg2bas  19587  crctcshwlkn0lem6  30386  wwlksnredwwlkn  30466  wwlksnextprop  30483  clwwlk1loop  30561  clwlkclwwlklem2fv1  30568  clwlkclwwlklem2fv2  30569  clwlkclwwlklem2a  30571  clwlkclwwlklem3  30574  clwwisshclwwslem  30587  clwwlknlbonbgr1  30612  clwwlkn1  30614  frcond1  30849  frgr1v  30854  nfrgr2v  30855  frgr3v  30858  n4cyclfrgr  30874  2clwwlk2clwwlklem  30929  wopprc  43990  mnurndlem1  45224  grtriclwlk3  48987  isubgr3stgrlem4  49011  gpgedgiov  49107  gpgedg2ov  49108  gpgedg2iv  49109  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  grlimedgnedg  49173  2arymaptf1  49709  rrx2xpref1o  49774